(<=> (Abelian-Group ?Domain ?Op ?Id)
(And (Group ?Domain ?Op ?Id) (Commutative ?Op ?Domain)))
(<=> (Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
(And (Abelian-Group ?Domain ?Plus-Op ?Zero-Id)
(Semigroup ?Domain ?Mult-Op ?One-Id)
(Distributes ?Mult-Op ?Plus-Op ?Domain)))
(<=> (Commutative-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
(And (Abelian-Group ?Domain ?Plus-Op ?Zero-Id)
(Abelian-Semigroup ?Domain ?Mult-Op ?One-Id)
(Distributes ?Mult-Op ?Plus-Op ?Domain)))
(<=> (Linear-Space ?Scalar-Domain
?Vector-Domain
?S-Zero
?S-One
?V-Zero
?Mult
?Add)
(And (Class ?Scalar-Domain)
(Class ?Vector-Domain)
(Field ?Scalar-Domain ?Add ?S-Zero ?Mult ?S-One)
(Abelian-Group ?Vector-Domain ?Add ?V-Zero)
(Forall (?S ?V)
(=> (And (Instance-Of ?S ?Scalar-Domain)
(Instance-Of ?V ?Vector-Domain))
(Instance-Of (Value ?Mult ?S ?V)
?Vector-Domain)))
(Forall (?S ?V1 ?V2)
(=> (And (Instance-Of ?S ?Scalar-Domain)
(Instance-Of ?V1 ?Vector-Domain)
(Instance-Of ?V2 ?Vector-Domain))
(= (Value ?Mult ?S (Value ?Add ?V1 ?V2))
(Value ?Add
(Value ?Mult ?S ?V1)
(Value ?Mult ?S ?V2)))))
(Forall (?S1 ?S2 ?V)
(=> (And (Instance-Of ?S1 ?Scalar-Domain)
(Instance-Of ?S2 ?Scalar-Domain)
(Instance-Of ?V ?Vector-Domain))
(= (Value ?Mult (Value ?Add ?S1 ?S2) ?V)
(Value ?Add
(Value ?Mult ?S1 ?V)
(Value ?Mult ?S2 ?V)))))
(Forall (?S1 ?S2 ?V)
(=> (And (Instance-Of ?S1 ?Scalar-Domain)
(Instance-Of ?S2 ?Scalar-Domain)
(Instance-Of ?V ?Vector-Domain))
(= (Value ?Mult (Value ?Mult ?S1 ?S2) ?V)
(Value ?Mult ?S1 (Value ?Mult ?S2 ?V)))))
(Forall (?V)
(=> (Instance-Of ?V ?Vector-Domain)
(And (= (Value ?Mult ?S-One ?V) ?V)
(= (Value ?Mult ?S-Zero ?V) ?V-Zero))))))