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 commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I 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 commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I 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 commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I 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 commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I 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 commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I 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 commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))
let Y be Element of Fin J; :: thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g))))) )
assume that
A1: F is commutative and
A2: F is associative and
A3: F is having_a_unity and
A4: F is having_an_inverseOp and
A5: G is_distributive_wrt F ; :: thesis: for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))

now :: thesis: for x being Element of I
for Y being Element of Fin J holds S₁[Y]

let x be Element of I; :: thesis: for Y being Element of Fin J holds S₁[Y]
defpred S₁[ Element of Fin J] means F $$ ([:{.x.},$1:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ($1,g)))));
A6: S₁[ {}. J]

proof

set z = the_unity_wrt F;
reconsider T = {}. [:I,J:] as Element of Fin [:I,J:] ;
A7: T = [:{x},({}. J):] by ZFMISC_1:90;
A8: dom <:f,((dom f) --> (the_unity_wrt F)):> = (dom f) /\ (dom ((dom f) --> (the_unity_wrt F))) by FUNCT_3:def 7
.= (dom f) /\ (dom f) by FUNCOP_1:13
.= dom f ;
( rng f c= D & rng ((dom f) --> (the_unity_wrt F)) c= D ) by RELAT_1:def 19;
then A9: [:(rng f),(rng ((dom f) --> (the_unity_wrt F))):] c= [:D,D:] by ZFMISC_1:96;
dom f = I by FUNCT_2:def 1;
then A10: x in dom <:f,((dom f) --> (the_unity_wrt F)):> by A8;
( dom G = [:D,D:] & rng <:f,((dom f) --> (the_unity_wrt F)):> c= [:(rng f),(rng ((dom f) --> (the_unity_wrt F))):] ) by FUNCT_2:def 1, FUNCT_3:51;
then x in dom (G * <:f,((dom f) --> (the_unity_wrt F)):>) by A10, A9, RELAT_1:27, XBOOLE_1:1;
then A11: x in dom (G [:] (f,(the_unity_wrt F))) by FUNCOP_1:def 4;
F $$ ({.x.},(G [:] (f,(F $$ (({}. J),g))))) = F $$ ({.x.},(G [:] (f,(the_unity_wrt F)))) by A1, A2, A3, SETWISEO:31
.= (G [:] (f,(the_unity_wrt F))) . x by A1, A2, SETWISEO:17
.= G . ((f . x),(the_unity_wrt F)) by A11, FUNCOP_1:27
.= the_unity_wrt F by A2, A3, A4, A5, FINSEQOP:66 ;
hence S₁[ {}. J] by A1, A2, A3, A7, SETWISEO:31; :: thesis: verum

end;

A12: for Y1 being Element of Fin J
for y being Element of J st S₁[Y1] holds
S₁[Y1 \/ {.y.}]

proof

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

per cases ( y in Y1 or not y in Y1 ) ;

suppose y in Y1 ; :: thesis: S₁[Y1 \/ {.y.}]

then Y1 \/ {y} = Y1 by ZFMISC_1:40;
hence S₁[Y1 \/ {.y.}] by A13; :: thesis: verum

end;

suppose not y in Y1 ; :: thesis: S₁[Y1 \/ {.y.}]

then A14: Y1 misses {y} by ZFMISC_1:50;
then A15: [:{x},Y1:] misses [:{x},s:] by ZFMISC_1:104;
thus F $$ ([:{.x.},(Y1 \/ {.y.}):],(G * (f,g))) = F $$ (([:{.x.},Y1:] \/ [:{.x.},s:]),(G * (f,g))) by ZFMISC_1:97
.= F . ((F $$ ([:{.x.},Y1:],(G * (f,g)))),(F $$ ([:{.x.},s:],(G * (f,g))))) by A1, A2, A3, A15, SETWOP_2:4
.= F . ((F $$ ({.x.},(G [:] (f,(F $$ (Y1,g)))))),(F $$ ({.x.},(G [:] (f,(F $$ (s,g))))))) by A1, A2, A13, Th24
.= F $$ ({.x.},(F .: ((G [:] (f,(F $$ (Y1,g)))),(G [:] (f,(F $$ (s,g))))))) by A1, A2, A3, SETWOP_2:10
.= F $$ ({.x.},(G [:] (f,(F . ((F $$ (Y1,g)),(F $$ (s,g))))))) by A5, FINSEQOP:36
.= F $$ ({.x.},(G [:] (f,(F $$ ((Y1 \/ {.y.}),g))))) by A1, A2, A3, A14, SETWOP_2:4 ; :: thesis: verum

end;

end;

end;

thus for Y being Element of Fin J holds S₁[Y] from SETWISEO:sch 4(A6, A12); :: thesis: verum

end;

hence for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g))))) ; :: thesis: verum