let D be non empty set ; :: thesis: for A, M being BinOp of D st M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for CE1, CE2, CE12 being non-empty non empty FinSequence of D * st CE12 = CE1 ^ CE2 holds
for S1 being Element of Fin (dom (App CE1))
for s2 being Element of dom (App CE2)
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12)))
let A, M be BinOp of D; :: thesis: ( M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A implies for CE1, CE2, CE12 being non-empty non empty FinSequence of D * st CE12 = CE1 ^ CE2 holds
for S1 being Element of Fin (dom (App CE1))
for s2 being Element of dom (App CE2)
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12))) )
assume A1: ( M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A ) ; :: thesis: for CE1, CE2, CE12 being non-empty non empty FinSequence of D * st CE12 = CE1 ^ CE2 holds
for S1 being Element of Fin (dom (App CE1))
for s2 being Element of dom (App CE2)
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12)))
let CE1, CE2, CE12 be non-empty non empty FinSequence of D * ; :: thesis: ( CE12 = CE1 ^ CE2 implies for S1 being Element of Fin (dom (App CE1))
for s2 being Element of dom (App CE2)
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12))) )
assume A2: CE12 = CE1 ^ CE2 ; :: thesis: for S1 being Element of Fin (dom (App CE1))
for s2 being Element of dom (App CE2)
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12)))
let S1 be Element of Fin (dom (App CE1)); :: thesis: for s2 being Element of dom (App CE2)
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12)))
let s2 be Element of dom (App CE2); :: thesis: for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12)))
let S12 be Element of Fin (dom (App CE12)); :: thesis: ( S12 = S1 ^ {s2} implies M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12))) )
assume A3: S12 = S1 ^ {s2} ; :: thesis: M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12)))
defpred S₁[ set ] means for S1 being Element of Fin (dom (App CE1))
for S12 being Element of Fin (dom (App CE12)) st S1 = $1 & S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)));
A4: S₁[ {}. (dom (App CE1))]

proof

let S1 be Element of Fin (dom (App CE1)); :: thesis: for S12 being Element of Fin (dom (App CE12)) st S1 = {}. (dom (App CE1)) & S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))
let S12 be Element of Fin (dom (App CE12)); :: thesis: ( S1 = {}. (dom (App CE1)) & S12 = S1 ^ {s2} implies M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) )
assume A5: ( S1 = {}. (dom (App CE1)) & S12 = S1 ^ {s2} ) ; :: thesis: M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))
S1 ^ {s2} = {}. (dom (App CE12)) by A5;
then A6: A $$ (S12,(M "**" (App CE12))) = the_unity_wrt A by A1, A5, SETWISEO:31;
A $$ (S1,(M "**" (App CE1))) = the_unity_wrt A by A5, A1, SETWISEO:31;
hence M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) by A6, A1, FINSEQOP:66; :: thesis: verum

end;

A7: 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 A8: ( S₁[B9] & not b in B9 ) ; :: thesis: S₁[B9 \/ {b}]
let S1 be Element of Fin (dom (App CE1)); :: thesis: for S12 being Element of Fin (dom (App CE12)) st S1 = B9 \/ {b} & S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))
let S12 be Element of Fin (dom (App CE12)); :: thesis: ( S1 = B9 \/ {b} & S12 = S1 ^ {s2} implies M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) )
assume A9: ( S1 = B9 \/ {b} & S12 = S1 ^ {s2} ) ; :: thesis: M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))
A10: S12 c= dom (App CE12) by FINSUB_1:def 5;
B9 c= S1 by XBOOLE_1:7, A9;
then B9 ^ {s2} c= S1 ^ {s2} by POLNOT_1:16;
then B9 ^ {s2} c= dom (App CE12) by A9, A10;
then reconsider Bs = B9 ^ {s2} as Element of Fin (dom (App CE12)) by FINSUB_1:def 5;
{b} c= S1 by XBOOLE_1:7, A9;
then {b} ^ {s2} c= S1 ^ {s2} by POLNOT_1:16;
then {b} ^ {s2} c= dom (App CE12) by A9, A10;
then reconsider bs = {.b.} ^ {.s2.} as Element of Fin (dom (App CE12)) by FINSUB_1:def 5;
b ^ s2 in doms CE12 by Th48, A2;
then reconsider BS2 = b ^ s2 as Element of dom (App CE12) by Def9;
A11: ( len ((App CE1) . b) >= 1 & len ((App CE2) . s2) >= 1 ) by NAT_1:14;
bs = {(b ^ s2)} by Th43;
then A12: A $$ (bs,(M "**" (App CE12))) = (M "**" (App CE12)) . BS2 by SETWISEO:17, A1
.= M "**" ((App CE12) . BS2) by Def10
.= M "**" (((App CE1) . b) ^ ((App CE2) . s2)) by A2, Th61
.= M . ((M "**" ((App CE1) . b)),(M "**" ((App CE2) . s2))) by A11, A1, FINSOP_1:5
.= M . (((M "**" (App CE1)) . b),(M "**" ((App CE2) . s2))) by Def10
.= M . (((M "**" (App CE1)) . b),((M "**" (App CE2)) . s2)) by Def10
.= M . ((A $$ ({.b.},(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) by SETWISEO:17, A1
.= M . ((A $$ ({.b.},(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) by SETWISEO:17, A1 ;
A13: B9 misses {b} by ZFMISC_1:50, A8;
A14: Bs misses bs

proof

assume Bs meets bs ; :: thesis: contradiction
then consider x being object such that
A15: ( x in Bs & x in bs ) by XBOOLE_0:3;
consider p1, q1 being FinSequence such that
A16: ( x = p1 ^ q1 & p1 in B9 & q1 in {s2} ) by A15, POLNOT_1:def 2;
consider p2, q2 being FinSequence such that
A17: ( x = p2 ^ q2 & p2 in {b} & q2 in {s2} ) by A15, POLNOT_1:def 2;
( q1 = s2 & s2 = q2 ) by A16, A17, TARSKI:def 1;
then p1 = p2 by A16, A17, FINSEQ_1:33;
hence contradiction by A16, A17, A8, TARSKI:def 1; :: thesis: verum

end;

S12 = Bs \/ bs by A9, Th42;
then A $$ (S12,(M "**" (App CE12))) = A . ((A $$ (Bs,(M "**" (App CE12)))),(A $$ (bs,(M "**" (App CE12))))) by A14, A1, SETWOP_2:4
.= A . ((M . ((A $$ (B9,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2)))))),(M . ((A $$ ({.b.},(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))))) by A8, A12
.= M . ((A . ((A $$ (B9,(M "**" (App CE1)))),(A $$ ({.b.},(M "**" (App CE1)))))),(A $$ ({.s2.},(M "**" (App CE2))))) by A1, BINOP_1:11
.= M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) by A9, A13, A1, SETWOP_2:4 ;
hence M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) ; :: thesis: verum

end;

for B being Element of Fin (dom (App CE1)) holds S₁[B] from SETWISEO:sch 2(A4, A7);
then M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ ({.s2.},(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) by A3;
hence M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12))) by SETWISEO:17, A1; :: thesis: verum