environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, FUNCT_1, BINOP_1, FUNCT_2, RELAT_1, FINSEQ_2, SETWISEO, XXREAL_0, CARD_1, ARYTM_3, FUNCOP_1, TARSKI, FUNCT_4, FINSUB_1, ORDINAL4, NAT_1, ARYTM_1, PARTFUN1, FINSOP_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, BINOP_1, PARTFUN1, FINSEQ_2, FINSEQ_1, FINSEQ_4, RELAT_1, RELSET_1, FUNCT_1, FINSUB_1, SETWISEO, FUNCT_2, NAT_1, FUNCOP_1, FUNCT_4, XXREAL_0;
definitions FUNCT_1, TARSKI, XBOOLE_0;
theorems BINOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2, NAT_1, SETWISEO, TARSKI, RELAT_1, FUNCOP_1, FUNCT_4, FINSUB_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1;
schemes FINSEQ_1, FINSEQ_2, NAT_1, FUNCT_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, FINSEQ_1, CARD_1, FINSEQ_2, NAT_1;
constructors HIDDEN, BINOP_1, PARTFUN1, FUNCOP_1, FUNCT_4, SETWISEO, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, FINSEQ_4, RELSET_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ;
expansions ;
Lm1:
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
Lm2:
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
Lm3:
for D being non empty set
for g being BinOp of D st g is having_a_unity holds
g "**" (<*> D) = the_unity_wrt g
Lm4:
for D being non empty set
for d being Element of D
for g being BinOp of D holds g "**" <*d*> = d
Lm5:
for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st len F >= 1 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
Lm6:
for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
Lm7:
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative holds
for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G
Lm8:
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D
for P being Permutation of (dom F) st g is having_a_unity & len F = 0 & G = F * P holds
g "**" F = g "**" G
Lm9:
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds
g "**" F = g "**" G
Lm10:
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
Lm11:
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F = 1 holds
g "**" F = F . 1
Lm12:
for D being non empty set
for F, G, H being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = g . ((F . k),(G . k)) ) holds
g "**" H = g . ((g "**" F),(g "**" G))
Lm13:
for D being non empty set
for F, G, H being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds
g "**" F = g . ((g "**" G),(g "**" H))