let D be non empty set ; :: thesis: for I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let I, J be non empty set ; :: thesis: for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let F, G be BinOp of D; :: thesis: for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let f be Function of I,D; :: thesis: for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let g be Function of J,D; :: thesis: for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let X be Element of Fin I; :: thesis: for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let Y be Element of Fin J; :: thesis: ( F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F implies F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g))))) )
assume that
A1: ( F is having_a_unity & F is commutative & F is associative ) and
A2: ( F is having_an_inverseOp & G is_distributive_wrt F ) ; :: thesis: F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
defpred S₁[ Element of Fin I] means F $$ ([:$1,Y:],(G * (f,g))) = F $$ ($1,(G [:] (f,(F $$ (Y,g)))));
A3: for X1 being Element of Fin I
for x being Element of I st S₁[X1] holds
S₁[X1 \/ {.x.}]

proof

let X1 be Element of Fin I; :: thesis: for x being Element of I st S₁[X1] holds
S₁[X1 \/ {.x.}]
let x be Element of I; :: thesis: ( S₁[X1] implies S₁[X1 \/ {.x.}] )
reconsider s = {.x.} as Element of Fin I ;
assume A4: F $$ ([:X1,Y:],(G * (f,g))) = F $$ (X1,(G [:] (f,(F $$ (Y,g))))) ; :: thesis: S₁[X1 \/ {.x.}]

now :: thesis: ( ( x in X1 & S₁[X1 \/ {.x.}] ) or ( not x in X1 & F $$ ([:(X1 \/ {.x.}),Y:],(G * (f,g))) = F $$ ((X1 \/ {.x.}),(G [:] (f,(F $$ (Y,g))))) ) )

per cases ( x in X1 or not x in X1 ) ;

case x in X1 ; :: thesis: S₁[X1 \/ {.x.}]

then X1 \/ {x} = X1 by ZFMISC_1:40;
hence S₁[X1 \/ {.x.}] by A4; :: thesis: verum

end;

case not x in X1 ; :: thesis: F $$ ([:(X1 \/ {.x.}),Y:],(G * (f,g))) = F $$ ((X1 \/ {.x.}),(G [:] (f,(F $$ (Y,g)))))

then A5: X1 misses {x} by ZFMISC_1:50;
then A6: [:X1,Y:] misses [:s,Y:] by ZFMISC_1:104;
thus F $$ ([:(X1 \/ {.x.}),Y:],(G * (f,g))) = F $$ (([:X1,Y:] \/ [:s,Y:]),(G * (f,g))) by ZFMISC_1:97
.= F . ((F $$ ([:X1,Y:],(G * (f,g)))),(F $$ ([:s,Y:],(G * (f,g))))) by A1, A6, SETWOP_2:4
.= F . ((F $$ (X1,(G [:] (f,(F $$ (Y,g)))))),(F $$ (s,(G [:] (f,(F $$ (Y,g))))))) by A1, A2, A4, Th25
.= F $$ ((X1 \/ {.x.}),(G [:] (f,(F $$ (Y,g))))) by A1, A5, SETWOP_2:4 ; :: thesis: verum

end;

end;

end;

hence S₁[X1 \/ {.x.}] ; :: thesis: verum

end;

A7: S₁[ {}. I]

proof

reconsider T = {}. [:I,J:] as Element of Fin [:I,J:] ;
T = [:({}. I),Y:] by ZFMISC_1:90;
then F $$ ([:({}. I),Y:],(G * (f,g))) = the_unity_wrt F by A1, SETWISEO:31;
hence S₁[ {}. I] by A1, SETWISEO:31; :: thesis: verum

end;

for X1 being Element of Fin I holds S₁[X1] from SETWISEO:sch 4(A7, A3);
hence F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g))))) ; :: thesis: verum