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

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:113;
A8: dom <:f,((dom f) --> (the_unity_wrt F)):> = (dom f) /\ (dom ((dom f) --> (the_unity_wrt F))) by FUNCT_3:def 8
.= (dom f) /\ (dom f) by FUNCOP_1:19
.= dom f ;
( {(the_unity_wrt F)} c= D & rng ((dom f) --> (the_unity_wrt F)) c= {(the_unity_wrt F)} ) by FUNCOP_1:19, ZFMISC_1:37;
then ( rng f c= D & rng ((dom f) --> (the_unity_wrt F)) c= D ) by RELAT_1:def 19, XBOOLE_1:1;
then A9: [:(rng f),(rng ((dom f) --> (the_unity_wrt F))):] c= [:D,D:] by ZFMISC_1:119;
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:71;
then x in dom (G * <:f,((dom f) --> (the_unity_wrt F)):>) by A10, A9, RELAT_1:46, 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:40
.= (G [:] f,(the_unity_wrt F)) . x by A1, A2, SETWISEO:26
.= G . (f . x),(the_unity_wrt F) by A11, FUNCOP_1:35
.= the_unity_wrt F by A2, A3, A4, A5, FINSEQOP:70 ;
hence S₁[ {}. J] by A1, A2, A3, A7, SETWISEO:40; :: 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:46;
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:56;
then A15: [:{x},Y1:] misses [:{x},s:] by ZFMISC_1:127;
thus F $$ [:{.x.},(Y1 \/ {.y.}):],(G * f,g) = F $$ ([:{.x.},Y1:] \/ [:{.x.},s:]),(G * f,g) by ZFMISC_1:120
.= F . (F $$ [:{.x.},Y1:],(G * f,g)),(F $$ [:{.x.},s:],(G * f,g)) by A1, A2, A3, A15, SETWOP_2:6
.= F . (F $$ {.x.},(G [:] f,(F $$ Y1,g))),(F $$ {.x.},(G [:] f,(F $$ s,g))) by A1, A2, A13, Th26
.= F $$ {.x.},(F .: (G [:] f,(F $$ Y1,g)),(G [:] f,(F $$ s,g))) by A1, A2, A3, SETWOP_2:12
.= F $$ {.x.},(G [:] f,(F . (F $$ Y1,g),(F $$ s,g))) by A5, FINSEQOP:37
.= F $$ {.x.},(G [:] f,(F $$ (Y1 \/ {.y.}),g)) by A1, A2, A3, A14, SETWOP_2:6 ; :: 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