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 Fin (dom (App CE2))
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = 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 Fin (dom (App CE2))
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) )
assume that
A1: ( M is commutative & M is associative ) and
A2: ( A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp ) and
A3: 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 Fin (dom (App CE2))
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = 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 Fin (dom (App CE2))
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) )
assume A4: CE12 = CE1 ^ CE2 ; :: thesis: for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2))
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))
let S1 be Element of Fin (dom (App CE1)); :: thesis: for S2 being Element of Fin (dom (App CE2))
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))
set aS1 = A $$ (S1,(M "**" (App CE1)));
defpred S₁[ Nat] means for S2 being Element of Fin (dom (App CE2))
for S12 being Element of Fin (dom (App CE12)) st card S2 = $1 & S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)));
A5: S₁[ 0 ]

proof

let S2 be Element of Fin (dom (App CE2)); :: thesis: for S12 being Element of Fin (dom (App CE12)) st card S2 = 0 & 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: ( card S2 = 0 & S12 = S1 ^ S2 implies M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) )
assume A6: ( card S2 = 0 & S12 = S1 ^ S2 ) ; :: thesis: M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))
S2 is empty by A6;
then A7: S1 ^ S2 = {}. (dom (App CE12)) ;
S2 = {}. (dom (App CE2)) by A6;
then A $$ (S2,(M "**" (App CE2))) = the_unity_wrt A by A2, SETWISEO:31;
then M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = the_unity_wrt A by A2, A3, FINSEQOP:66;
hence M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) by A7, A6, A2, SETWISEO:31; :: thesis: verum

end;

A8: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: S₁[n] ; :: thesis: S₁[n + 1]
let S2 be Element of Fin (dom (App CE2)); :: thesis: for S12 being Element of Fin (dom (App CE12)) st card S2 = n + 1 & 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: ( card S2 = n + 1 & S12 = S1 ^ S2 implies M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) )
assume A10: ( card S2 = n + 1 & S12 = S1 ^ S2 ) ; :: thesis: M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))
not S2 is empty by A10;
then consider s being object such that
A11: s in S2 ;
S2 c= dom (App CE2) by FINSUB_1:def 5;
then reconsider s = s as Element of dom (App CE2) by A11;
S2 c= dom (App CE2) by FINSUB_1:def 5;
then S2 \ {s} c= dom (App CE2) ;
then reconsider S2s = S2 \ {s} as Element of Fin (dom (App CE2)) by FINSUB_1:def 5;
A12: card S2s = n by A10, A11, STIRL2_1:55;
A13: not s in S2s by ZFMISC_1:56;
A14: S2s \/ {s} = S2 by A11, ZFMISC_1:116;
A15: S12 c= dom (App CE12) by FINSUB_1:def 5;
S1 ^ S2s c= S1 ^ S2 by POLNOT_1:16;
then S1 ^ S2s c= dom (App CE12) by A15, A10;
then reconsider S1S2s = S1 ^ S2s as Element of Fin (dom (App CE12)) by FINSUB_1:def 5;
{s} c= S2 by A11, ZFMISC_1:31;
then S1 ^ {s} c= S1 ^ S2 by POLNOT_1:16;
then S1 ^ {s} c= dom (App CE12) by A15, A10;
then reconsider S1s = S1 ^ {.s.} as Element of Fin (dom (App CE12)) by FINSUB_1:def 5;
A16: S1s misses S1S2s

proof

assume S1s meets S1S2s ; :: thesis: contradiction
then consider x being object such that
A17: ( x in S1s & x in S1S2s ) by XBOOLE_0:3;
consider p1, q1 being FinSequence such that
A18: ( x = p1 ^ q1 & p1 in S1 & q1 in {s} ) by A17, POLNOT_1:def 2;
consider p2, q2 being FinSequence such that
A19: ( x = p2 ^ q2 & p2 in S1 & q2 in S2 \ {s} ) by A17, POLNOT_1:def 2;
S1 c= dom (App CE1) by FINSUB_1:def 5;
then ( p1 in dom (App CE1) & p2 in dom (App CE1) ) by A18, A19;
then ( len p1 = len CE1 & len CE1 = len p2 ) by Th47;
then ( p1 = (p1 ^ q1) | (len p1) & (p1 ^ q1) | (len p1) = p2 ) by A18, A19, FINSEQ_5:23;
then ( s = q1 & q1 = q2 ) by A18, A19, FINSEQ_1:33, TARSKI:def 1;
hence contradiction by A19, ZFMISC_1:56; :: thesis: verum

end;

A20: A $$ (S12,(M "**" (App CE12))) = A $$ ((S1s \/ S1S2s),(M "**" (App CE12))) by A10, A14, Th41
.= A . ((A $$ (S1s,(M "**" (App CE12)))),(A $$ (S1S2s,(M "**" (App CE12))))) by SETWOP_2:4, A16, A2 ;
A $$ (S12,(M "**" (App CE12))) = A . ((A $$ (S1s,(M "**" (App CE12)))),(M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2s,(M "**" (App CE2))))))) by A9, A12, A20
.= A . ((M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s))),(M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2s,(M "**" (App CE2))))))) by Th92, A1, A2, A3, A4
.= A . ((M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2s,(M "**" (App CE2)))))),(M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s)))) by A2, BINOP_1:def 2
.= M . ((A $$ (S1,(M "**" (App CE1)))),(A . ((A $$ (S2s,(M "**" (App CE2)))),((M "**" (App CE2)) . s)))) by BINOP_1:11, A3
.= M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) by A14, A13, SETWOP_2:2, A2 ;
hence M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) ; :: thesis: verum

end;

let S2 be Element of Fin (dom (App CE2)); :: thesis: for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A8);
then S₁[ card S2] ;
hence for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12))) ; :: thesis: verum