let D be non empty set ; :: thesis: for A, M being BinOp of D
for f being FinSequence of D
for F1 being finite set st A is having_a_unity & A is commutative & A is associative holds
for E1 being Enumeration of F1 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let A, M be BinOp of D; :: thesis: for f being FinSequence of D
for F1 being finite set st A is having_a_unity & A is commutative & A is associative holds
for E1 being Enumeration of F1 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let f be FinSequence of D; :: thesis: for F1 being finite set st A is having_a_unity & A is commutative & A is associative holds
for E1 being Enumeration of F1 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let F1 be finite set ; :: thesis: ( A is having_a_unity & A is commutative & A is associative implies for E1 being Enumeration of F1 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A1: ( A is having_a_unity & A is commutative & A is associative ) ; :: thesis: for E1 being Enumeration of F1 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let E1 be Enumeration of F1; :: thesis: ( union F1 c= dom f implies for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A2: union F1 c= dom f ; :: thesis: for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let g be Permutation of (dom f); :: thesis: for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let gE1 be Enumeration of (.: g) .: F1; :: thesis: ( gE1 = (.: g) * E1 implies for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A3: gE1 = (.: g) * E1 ; :: thesis: for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let fg be FinSequence of D; :: thesis: ( fg = f * (g ") implies for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A4: fg = f * (g ") ; :: thesis: for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let CE1, CE2 be non-empty non empty FinSequence of D * ; :: thesis: ( CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 implies for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A5: ( CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 ) ; :: thesis: for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
defpred S₁[ set ] means for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = $1 & S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)));
A6: S₁[ {}. (dom (App CE1))]

proof

let S1 be Element of Fin (dom (App CE1)); :: thesis: for S2 being Element of Fin (dom (App CE2)) st S1 = {}. (dom (App CE1)) & S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let S2 be Element of Fin (dom (App CE2)); :: thesis: ( S1 = {}. (dom (App CE1)) & S2 = { (g * s) where s is FinSequence of NAT : s in S1 } implies A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A7: ( S1 = {}. (dom (App CE1)) & S2 = { (g * s) where s is FinSequence of NAT : s in S1 } ) ; :: thesis: A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
S2 = {}

proof

assume S2 <> {} ; :: thesis: contradiction
then consider x being object such that
A8: x in S2 by XBOOLE_0:def 1;
ex s being FinSequence of NAT st
( x = g * s & s in S1 ) by A8, A7;
hence contradiction by A7; :: thesis: verum

end;

then S2 = {}. (dom (App CE2)) ;
then A $$ (S2,(M "**" (App CE2))) = the_unity_wrt A by A1, SETWISEO:31
.= A $$ (S1,(M "**" (App CE1))) by A7, A1, SETWISEO:31 ;
hence A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) ; :: thesis: verum

end;

A9: for B9 being Element of Fin (dom (App CE1))
for b being Element of dom (App CE1) st S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]

proof

let B9 be Element of Fin (dom (App CE1)); :: thesis: for b being Element of dom (App CE1) st S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]
let b be Element of dom (App CE1); :: thesis: ( S₁[B9] & not b in B9 implies S₁[B9 \/ {b}] )
assume A10: ( S₁[B9] & not b in B9 ) ; :: thesis: S₁[B9 \/ {b}]
let S1 be Element of Fin (dom (App CE1)); :: thesis: for S2 being Element of Fin (dom (App CE2)) st S1 = B9 \/ {b} & S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let S2 be Element of Fin (dom (App CE2)); :: thesis: ( S1 = B9 \/ {b} & S2 = { (g * s) where s is FinSequence of NAT : s in S1 } implies A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A11: ( S1 = B9 \/ {b} & S2 = { (g * s) where s is FinSequence of NAT : s in S1 } ) ; :: thesis: A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
set B2 = { (g * s) where s is FinSequence of NAT : s in B9 } ;
reconsider B2 = { (g * s) where s is FinSequence of NAT : s in B9 } as Element of Fin (dom (App CE2)) by A2, A3, A4, A5, Th100;
b in doms CE1 ;
then reconsider c = b as FinSequence of NAT by FINSEQ_1:def 11;
A12: B2 c= S2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B2 or y in S2 )
assume A13: y in B2 ; :: thesis: y in S2
consider s being FinSequence of NAT such that
A14: ( y = g * s & s in B9 ) by A13;
s in S1 by A14, A11, XBOOLE_0:def 3;
hence y in S2 by A14, A11; :: thesis: verum

end;

c in S1 by A11, ZFMISC_1:136;
then A15: g * c in S2 by A11;
then A16: {(g * b)} c= S2 by ZFMISC_1:31;
S2 c= dom (App CE2) by FINSUB_1:def 5;
then reconsider gc = g * c as Element of dom (App CE2) by A15;
A17: dom f = dom g by FUNCT_2:52;
A18: rng c c= dom f

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in dom f )
assume A19: y in rng c ; :: thesis: y in dom f
consider x being object such that
A20: ( x in dom c & c . x = y ) by A19, FUNCT_1:def 3;
A21: c . x in dom (CE1 . x) by A20, Th47;
then x in dom CE1 by RELAT_1:38, FUNCT_1:def 2;
then CE1 . x = SignGen (f,A,(E1 . x)) by A5, Th80;
hence y in dom f by A20, A21, Def11; :: thesis: verum

end;

A22: not gc in B2

proof

assume gc in B2 ; :: thesis: contradiction
then consider s being FinSequence of NAT such that
A23: ( gc = g * s & s in B9 ) ;
A24: rng s c= dom f

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in dom f )
assume A25: y in rng s ; :: thesis: y in dom f
consider x being object such that
A26: ( x in dom s & s . x = y ) by A25, FUNCT_1:def 3;
B9 c= dom (App CE1) by FINSUB_1:def 5;
then s in dom (App CE1) by A23;
then A27: s . x in dom (CE1 . x) by A26, Th47;
then x in dom CE1 by RELAT_1:38, FUNCT_1:def 2;
then CE1 . x = SignGen (f,A,(E1 . x)) by A5, Th80;
hence y in dom f by A26, A27, Def11; :: thesis: verum

end;

(g ") * gc = ((g ") * g) * s by A23, RELAT_1:36;
then ( ((g ") * g) * c = ((g ") * g) * s & (g ") * g = id (dom g) ) by RELAT_1:36, FUNCT_1:39;
then (id (dom g)) * c = s by A24, A17, RELAT_1:53;
hence contradiction by A10, A23, A18, A17, RELAT_1:53; :: thesis: verum

end;

S2 c= B2 \/ {(g * b)}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S2 or y in B2 \/ {(g * b)} )
assume A28: y in S2 ; :: thesis: y in B2 \/ {(g * b)}
consider s being FinSequence of NAT such that
A29: ( y = g * s & s in S1 ) by A28, A11;
( s in B9 or s = c ) by A11, A29, ZFMISC_1:136;
then ( y in B2 or y in {(g * b)} ) by A29, ZFMISC_1:31;
hence y in B2 \/ {(g * b)} by XBOOLE_0:def 3; :: thesis: verum

end;

then A30: B2 \/ {gc} = S2 by A16, A12, XBOOLE_1:8;
( dom (g ") = dom f & dom f = rng (g ") ) by FUNCT_2:52, FUNCT_2:def 3;
then A31: dom (f * (g ")) = dom f by RELAT_1:27;
A32: fg = (f * (g ")) | (dom fg) by A4;
A33: g .: (dom f) c= dom fg by A31, A4;
(App CE1) . c = (App CE2) . gc by A3, A5, A2, A33, A32, Th99, A18, A17;
then (M "**" (App CE1)) . c = M "**" ((App CE2) . gc) by Def10
.= (M "**" (App CE2)) . gc by Def10 ;
hence A $$ (S1,(M "**" (App CE1))) = A . ((A $$ (B9,(M "**" (App CE1)))),((M "**" (App CE2)) . gc)) by A1, A10, A11, SETWOP_2:2
.= A . ((A $$ (B2,(M "**" (App CE2)))),((M "**" (App CE2)) . gc)) by A10
.= A $$ (S2,(M "**" (App CE2))) by A30, A1, A22, SETWOP_2:2 ;
:: thesis: verum

end;

for B being Element of Fin (dom (App CE1)) holds S₁[B] from SETWISEO:sch 2(A6, A9);
hence for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) ; :: thesis: verum