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 st F is commutative & F is associative & F is having_a_unity holds
for x being Element of I
for y being Element of J 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 st F is commutative & F is associative & F is having_a_unity holds
for x being Element of I
for y being Element of J 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 st F is commutative & F is associative & F is having_a_unity holds
for x being Element of I
for y being Element of J 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 st F is commutative & F is associative & F is having_a_unity holds
for x being Element of I
for y being Element of J holds F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ {.y.},g))
let g be Function of J,D; :: thesis: ( F is commutative & F is associative & F is having_a_unity implies for x being Element of I
for y being Element of J holds F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ {.y.},g)) )
assume A1: ( F is commutative & F is associative & F is having_a_unity ) ; :: thesis: for x being Element of I
for y being Element of J holds F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ {.y.},g))
reconsider G = G as Function of [:D,D:],D ;
A2: dom (G * f,g) = [:I,J:] by FUNCT_2:def 1;

now

let x be Element of I; :: thesis: for y being Element of J holds F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ {.y.},g))
let y be Element of J; :: thesis: F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ {.y.},g))
A3: [x,y] in [:I,J:] by ZFMISC_1:106;
reconsider u = [x,y] as Element of [:I,J:] by ZFMISC_1:106;
A4: F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.u.},(G * f,g) by ZFMISC_1:35
.= (G * f,g) . x,y by A1, SETWISEO:26
.= G . (f . x),(g . y) by A2, A3, FINSEQOP:82 ;
reconsider z = g . y as Element of D ;
A5: dom f = I by FUNCT_2:def 1;
dom <:f,((dom f) --> z):> = (dom f) /\ (dom ((dom f) --> z)) by FUNCT_3:def 8
.= (dom f) /\ (dom f) by FUNCOP_1:19
.= dom f ;
then A6: x in dom <:f,((dom f) --> z):> by A5;
A7: rng f c= D by RELAT_1:def 19;
A8: {z} c= D by ZFMISC_1:37;
rng ((dom f) --> z) c= {z} by FUNCOP_1:19;
then A9: rng ((dom f) --> z) c= D by A8, XBOOLE_1:1;
A10: dom G = [:D,D:] by FUNCT_2:def 1;
A11: rng <:f,((dom f) --> z):> c= [:(rng f),(rng ((dom f) --> z)):] by FUNCT_3:71;
[:(rng f),(rng ((dom f) --> z)):] c= [:D,D:] by A7, A9, ZFMISC_1:119;
then x in dom (G * <:f,((dom f) --> z):>) by A6, A10, A11, RELAT_1:46, XBOOLE_1:1;
then A12: x in dom (G [:] f,z) by FUNCOP_1:def 4;
F $$ {.x.},(G [:] f,(F $$ {.y.},g)) = (G [:] f,(F $$ {.y.},g)) . x by A1, SETWISEO:26
.= (G [:] f,(g . y)) . x by A1, SETWISEO:26
.= G . (f . x),(g . y) by A12, FUNCOP_1:35 ;
hence F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ {.y.},g)) by A4; :: thesis: verum

end;

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