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 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 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 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 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 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 ) ; :: 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 z = g . y as Element of D ;
reconsider u = [x,y] as Element of [:I,J:] by ZFMISC_1:106;
A4: 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 ;
( {z} c= D & rng ((dom f) --> z) c= {z} ) by FUNCOP_1:19, ZFMISC_1:37;
then ( rng f c= D & rng ((dom f) --> z) c= D ) by RELAT_1:def 19, XBOOLE_1:1;
then A5: [:(rng f),(rng ((dom f) --> z)):] c= [:D,D:] by ZFMISC_1:119;
dom f = I by FUNCT_2:def 1;
then A6: x in dom <:f,((dom f) --> z):> by A4;
( dom G = [:D,D:] & rng <:f,((dom f) --> z):> c= [:(rng f),(rng ((dom f) --> z)):] ) by FUNCT_2:def 1, FUNCT_3:71;
then x in dom (G * <:f,((dom f) --> z):>) by A6, A5, RELAT_1:46, XBOOLE_1:1;
then A7: x in dom (G [:] f,z) by FUNCOP_1:def 4;
A8: 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 A7, FUNCOP_1:35 ;
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 ;
hence F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ {.y.},g)) by A8; :: 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