let D be non empty set ; :: thesis: for A, M being BinOp of D st A is commutative & A is associative & A is having_a_unity & M is commutative & M is_distributive_wrt A & ( for d being Element of D holds M . ((the_unity_wrt A),d) = the_unity_wrt A ) holds
for X, Y being non empty finite set
for f being Function of X,D
for g being Function of Y,D
for a being Element of Fin X
for b being Element of Fin Y holds A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)))
let A, M be BinOp of D; :: thesis: ( A is commutative & A is associative & A is having_a_unity & M is commutative & M is_distributive_wrt A & ( for d being Element of D holds M . ((the_unity_wrt A),d) = the_unity_wrt A ) implies for X, Y being non empty finite set
for f being Function of X,D
for g being Function of Y,D
for a being Element of Fin X
for b being Element of Fin Y holds A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g))) )
assume that
A1: ( A is commutative & A is associative & A is having_a_unity & M is commutative & M is_distributive_wrt A ) and
A2: for d being Element of D holds M . ((the_unity_wrt A),d) = the_unity_wrt A ; :: thesis: for X, Y being non empty finite set
for f being Function of X,D
for g being Function of Y,D
for a being Element of Fin X
for b being Element of Fin Y holds A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)))
let X, Y be non empty finite set ; :: thesis: for f being Function of X,D
for g being Function of Y,D
for a being Element of Fin X
for b being Element of Fin Y holds A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)))
let f be Function of X,D; :: thesis: for g being Function of Y,D
for a being Element of Fin X
for b being Element of Fin Y holds A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)))
let g be Function of Y,D; :: thesis: for a being Element of Fin X
for b being Element of Fin Y holds A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)))
set m = M * (f,g);
defpred S₁[ set ] means for a being Element of Fin X
for b being Element of Fin Y st a = $1 holds
A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)));
A3: S₁[ {}. X]

proof

let a be Element of Fin X; :: thesis: for b being Element of Fin Y st a = {}. X holds
A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)))
let b be Element of Fin Y; :: thesis: ( a = {}. X implies A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g))) )
assume A4: a = {}. X ; :: thesis: A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)))
[:({}. X),b:] = {}. [:X,Y:] by ZFMISC_1:90;
then A5: A $$ ([:({}. X),b:],(M * (f,g))) = the_unity_wrt A by A1, SETWISEO:31;
A $$ (({}. X),f) = the_unity_wrt A by A1, SETWISEO:31;
hence A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g))) by A4, A2, A5; :: thesis: verum

end;

A6: for E being Element of Fin X
for e being Element of X st S₁[E] & not e in E holds
S₁[E \/ {e}]

proof

let E be Element of Fin X; :: thesis: for e being Element of X st S₁[E] & not e in E holds
S₁[E \/ {e}]
let e be Element of X; :: thesis: ( S₁[E] & not e in E implies S₁[E \/ {e}] )
assume A7: ( S₁[E] & not e in E ) ; :: thesis: S₁[E \/ {e}]
defpred S₂[ set ] means for B being Element of Fin Y st B = $1 holds
A $$ ([:{.e.},B:],(M * (f,g))) = M . ((A $$ ({.e.},f)),(A $$ (B,g)));
A8: S₂[ {}. Y]

proof

let B be Element of Fin Y; :: thesis: ( B = {}. Y implies A $$ ([:{.e.},B:],(M * (f,g))) = M . ((A $$ ({.e.},f)),(A $$ (B,g))) )
assume A9: B = {}. Y ; :: thesis: A $$ ([:{.e.},B:],(M * (f,g))) = M . ((A $$ ({.e.},f)),(A $$ (B,g)))
A10: [:{.e.},({}. Y):] = {}. [:X,Y:] ;
M . ((A $$ ({.e.},f)),(A $$ (B,g))) = M . ((A $$ (B,g)),(A $$ ({.e.},f))) by A1, BINOP_1:def 2
.= M . ((the_unity_wrt A),(A $$ ({.e.},f))) by A9, A1, SETWISEO:31
.= the_unity_wrt A by A2 ;
hence A $$ ([:{.e.},B:],(M * (f,g))) = M . ((A $$ ({.e.},f)),(A $$ (B,g))) by A10, A9, A1, SETWISEO:31; :: thesis: verum

end;

A11: for B being Element of Fin Y
for b being Element of Y st S₂[B] & not b in B holds
S₂[B \/ {b}]

proof

let B be Element of Fin Y; :: thesis: for b being Element of Y st S₂[B] & not b in B holds
S₂[B \/ {b}]
let b be Element of Y; :: thesis: ( S₂[B] & not b in B implies S₂[B \/ {b}] )
assume A12: ( S₂[B] & not b in B ) ; :: thesis: S₂[B \/ {b}]
let Bb be Element of Fin Y; :: thesis: ( Bb = B \/ {b} implies A $$ ([:{.e.},Bb:],(M * (f,g))) = M . ((A $$ ({.e.},f)),(A $$ (Bb,g))) )
assume A13: Bb = B \/ {b} ; :: thesis: A $$ ([:{.e.},Bb:],(M * (f,g))) = M . ((A $$ ({.e.},f)),(A $$ (Bb,g)))
A14: B misses {.b.} by A12, ZFMISC_1:50;
then A15: [:{.e.},B:] misses [:{.e.},{.b.}:] by ZFMISC_1:104;
A16: {[e,b]} = [:{.e.},{.b.}:] by ZFMISC_1:29;
reconsider eb = [e,b] as Element of [:X,Y:] ;
A17: A $$ ([:{.e.},{.b.}:],(M * (f,g))) = (M * (f,g)) . eb by A16, A1, SETWISEO:17
.= (M * (f,g)) . (e,b) by BINOP_1:def 1
.= M . ((f . e),(g . b)) by FINSEQOP:81
.= M . ((A $$ ({.e.},f)),(g . b)) by A1, SETWISEO:17
.= M . ((A $$ ({.e.},f)),(A $$ ({.b.},g))) by A1, SETWISEO:17 ;
[:{.e.},B:] \/ [:{.e.},{.b.}:] = [:{.e.},Bb:] by A13, ZFMISC_1:97;
hence A $$ ([:{.e.},Bb:],(M * (f,g))) = A . ((A $$ ([:{.e.},B:],(M * (f,g)))),(A $$ ([:{.e.},{.b.}:],(M * (f,g))))) by A15, A1, SETWOP_2:4
.= A . ((M . ((A $$ ({.e.},f)),(A $$ (B,g)))),(M . ((A $$ ({.e.},f)),(A $$ ({.b.},g))))) by A12, A17
.= M . ((A $$ ({.e.},f)),(A . ((A $$ (B,g)),(A $$ ({.b.},g))))) by A1, BINOP_1:11
.= M . ((A $$ ({.e.},f)),(A $$ (Bb,g))) by A13, A1, SETWOP_2:4, A14 ;
:: thesis: verum

end;

A18: for B being Element of Fin Y holds S₂[B] from SETWISEO:sch 2(A8, A11);
let Q be Element of Fin X; :: thesis: for b being Element of Fin Y st Q = E \/ {e} holds
A $$ ([:Q,b:],(M * (f,g))) = M . ((A $$ (Q,f)),(A $$ (b,g)))
let B be Element of Fin Y; :: thesis: ( Q = E \/ {e} implies A $$ ([:Q,B:],(M * (f,g))) = M . ((A $$ (Q,f)),(A $$ (B,g))) )
assume A19: Q = E \/ {e} ; :: thesis: A $$ ([:Q,B:],(M * (f,g))) = M . ((A $$ (Q,f)),(A $$ (B,g)))
A20: E misses {.e.} by A7, ZFMISC_1:50;
then A21: [:E,B:] misses [:{.e.},B:] by ZFMISC_1:104;
[:E,B:] \/ [:{.e.},B:] = [:Q,B:] by A19, ZFMISC_1:97;
hence A $$ ([:Q,B:],(M * (f,g))) = A . ((A $$ ([:E,B:],(M * (f,g)))),(A $$ ([:{.e.},B:],(M * (f,g))))) by A21, A1, SETWOP_2:4
.= A . ((M . ((A $$ (E,f)),(A $$ (B,g)))),(A $$ ([:{.e.},B:],(M * (f,g))))) by A7
.= A . ((M . ((A $$ (E,f)),(A $$ (B,g)))),(M . ((A $$ ({.e.},f)),(A $$ (B,g))))) by A18
.= M . ((A . ((A $$ (E,f)),(A $$ ({.e.},f)))),(A $$ (B,g))) by A1, BINOP_1:11
.= M . ((A $$ (Q,f)),(A $$ (B,g))) by A19, A1, A20, SETWOP_2:4 ;
:: thesis: verum

end;

for E being Element of Fin X holds S₁[E] from SETWISEO:sch 2(A3, A6);
hence for a being Element of Fin X
for b being Element of Fin Y holds A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g))) ; :: thesis: verum