environ
vocabularies HIDDEN, RLVECT_1, ALGSTR_0, XBOOLE_0, STRUCT_0, VECTSP_1, SUPINF_2, BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, FINSEQOP, ARYTM_1, RELAT_1, GROUP_1, NAT_1, FINSEQ_2, CARD_3, FUNCOP_1, SETWISEO, ZFMISC_1, PARTFUN1, TARSKI, FINSEQ_1, MESFUNC1, MCART_1, FUNCT_6, GROUP_2, NUMBERS, PRVECT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, CARD_3, RELAT_1, FUNCT_1, STRUCT_0, ALGSTR_0, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCOP_1, RLVECT_1, GROUP_1, VECTSP_1, FINSEQOP, FINSEQ_1, FUNCT_6, SETWISEO, FINSEQ_2;
definitions BINOP_1, FINSEQOP, VECTSP_1, STRUCT_0, RELAT_1, RLVECT_1, ALGSTR_0, FUNCOP_1;
theorems BINOP_1, FUNCT_1, FUNCT_2, FUNCT_3, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQOP, FUNCOP_1, VECTSP_1, ZFMISC_1, SETWISEO, TARSKI, CARD_3, FUNCT_6, RLVECT_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, FVSUM_1, GROUP_1, CARD_1, XTUPLE_0;
schemes FUNCT_1, BINOP_1, FUNCT_2, FINSEQ_1, CLASSES1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSEQ_1, FINSEQ_2, CARD_3, STRUCT_0, VECTSP_1, RELSET_1, CARD_1;
constructors HIDDEN, PARTFUN1, BINOP_1, FUNCT_3, SETWISEO, FUNCT_5, CARD_3, FINSEQOP, FUNCT_6, VECTSP_1, RLVECT_1, RELSET_1, FINSEQ_2, GROUP_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities BINOP_1, VECTSP_1, STRUCT_0, ALGSTR_0, FUNCOP_1;
expansions BINOP_1, FINSEQOP, RLVECT_1;
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
by BINOP_1:3;
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
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;
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;
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;