let D be non empty set ; :: thesis:
let A, M be BinOp of D; :: thesis:
let f be FinSequence of D; :: thesis:
let F be finite set ; :: thesis:
assume that
A1: ( M is commutative & M is associative ) and
A2: ( A is having_a_unity & A is commutative & A is associative ) ; :: thesis:
let E be Enumeration of F; :: thesis:
let p be Permutation of (dom E); :: thesis:
assume A3: ( M is having_a_unity or len E >= 1 ) ; :: thesis:
let CE, CEp be non-empty non empty FinSequence of D * ; :: thesis:
assume A4: ( CE = (SignGenOp (f,A,F)) * E & CEp = (SignGenOp (f,A,F)) * (E * p) ) ; :: thesis:
defpred S₁[ set ] means for S being Element of Fin (dom (App CE))
for Sp being Element of Fin (dom (App CEp)) st S = $1 & Sp = { (s * p) where s is FinSequence of NAT : s in S } holds
A $$ (S,(M "**" (App CE))) = A $$ (Sp,(M "**" (App CEp)));
A5: ( dom p = dom E & dom E = rng p ) by FUNCT_2:52, FUNCT_2:def 3;
A6: S₁[ {}. (dom (App CE))]

let S be Element of Fin (dom (App CE)); :: thesis:
let Sp be Element of Fin (dom (App CEp)); :: thesis:
assume A7: ( S = {}. (dom (App CE)) & Sp = { (s * p) where s is FinSequence of NAT : s in S } ) ; :: thesis:
Sp = {}

end;

then Sp = {}. (dom (App CEp)) ;
then A $$ (Sp,(M "**" (App CEp))) = the_unity_wrt A by A2, SETWISEO:31
.= A $$ (S,(M "**" (App CE))) by A7, A2, SETWISEO:31 ;
hence A $$ (S,(M "**" (App CE))) = A $$ (Sp,(M "**" (App CEp))) ; :: thesis:

end;

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

let B9 be Element of Fin (dom (App CE)); :: thesis:
let b be Element of dom (App CE); :: thesis:
assume A10: ( S₁[B9] & not b in B9 ) ; :: thesis:
let S1 be Element of Fin (dom (App CE)); :: thesis:
let S2 be Element of Fin (dom (App CEp)); :: thesis:
assume A11: ( S1 = B9 \/ {b} & S2 = { (s * p) where s is FinSequence of NAT : s in S1 } ) ; :: thesis:
set B2 = { (s * p) where s is FinSequence of NAT : s in B9 } ;
reconsider B2 = { (s * p) where s is FinSequence of NAT : s in B9 } as Element of Fin (dom (App CEp)) by A4, Th113;
A12: ( len b = len CE & len CE = len E ) by Th47, A4, CARD_1:def 7;
then A13: dom E = dom b by FINSEQ_3:30;
b in doms CE ;
then reconsider c = b as FinSequence of NAT by FINSEQ_1:def 11;
A14: B2 c= S2

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

end;

end;

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

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

end;

then A25: B2 \/ {cp} = S2 by A18, A14, XBOOLE_1:8;
(M "**" (App CE)) . c = (M "**" (App CEp)) . cp by Th112, A1, A4, A12, A3;
hence A $$ (S1,(M "**" (App CE))) = A . ((A $$ (B9,(M "**" (App CE)))),((M "**" (App CEp)) . cp)) by A2, A10, A11, SETWOP_2:2
.= A . ((A $$ (B2,(M "**" (App CEp)))),((M "**" (App CEp)) . cp)) by A10
.= A $$ (S2,(M "**" (App CEp))) by A25, A2, A19, SETWOP_2:2 ;
:: thesis:

end;

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