begin
deffunc H1( 1-sorted ) -> set = the carrier of $1;
deffunc H2( addLoopStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1;
deffunc H3( non empty addLoopStr ) -> Element of bool [: the carrier of $1, the carrier of $1:] = comp $1;
deffunc H4( addLoopStr ) -> Element of the carrier of $1 = 0. $1;
Lm1:
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds comp G is_an_inverseOp_wrt the addF of G
Lm2:
for GS being non empty addLoopStr st the addF of GS is commutative & the addF of GS is associative holds
( GS is Abelian & GS is add-associative )
Lm3:
for GS being non empty addLoopStr st 0. GS is_a_unity_wrt the addF of GS holds
GS is right_zeroed
Lm4:
for F being Field holds the multF of F is associative
Lm5:
for F being Field holds the multF of F is_distributive_wrt the addF of F
begin
definition
let D be non
empty set ;
let F be
BinOp of
D;
let n be
Nat;
existence
ex b1 being BinOp of (n -tuples_on D) st
for x, y being Element of n -tuples_on D holds b1 . (x,y) = F .: (x,y)
uniqueness
for b1, b2 being BinOp of (n -tuples_on D) st ( for x, y being Element of n -tuples_on D holds b1 . (x,y) = F .: (x,y) ) & ( for x, y being Element of n -tuples_on D holds b2 . (x,y) = F .: (x,y) ) holds
b1 = b2
end;
begin
definition
let F be
Field;
let n be
Nat;
existence
ex b1 being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) st
for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . (x,v) = the multF of F [;] (x,v)
uniqueness
for b1, b2 being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) st ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . (x,v) = the multF of F [;] (x,v) ) & ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b2 . (x,v) = the multF of F [;] (x,v) ) holds
b1 = b2
end;
begin
begin
definition
let a be
Domain-Sequence;
let b be
BinOps of
a;
existence
ex b1 being BinOp of (product a) st
for f, g being Element of product a
for i being Element of dom a holds (b1 . (f,g)) . i = (b . i) . ((f . i),(g . i))
uniqueness
for b1, b2 being BinOp of (product a) st ( for f, g being Element of product a
for i being Element of dom a holds (b1 . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) & ( for f, g being Element of product a
for i being Element of dom a holds (b2 . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) holds
b1 = b2
end;
begin