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

now

let x be Element of I; :: thesis: for y being Element of J holds F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.y.},(G [;] (F $$ {.x.},f),g)
let y be Element of J; :: thesis: F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ {.y.},(G [;] (F $$ {.x.},f),g)
thus F $$ [:{.x.},{.y.}:],(G * f,g) = F $$ [:{.y.},{.x.}:],(G * g,f) by A1, A2, Th25
.= F $$ {.y.},(G [:] g,(F $$ {.x.},f)) by A1, Th26
.= F $$ {.y.},(G [;] (F $$ {.x.},f),g) by A2, FUNCOP_1:79 ; :: thesis: verum

end;

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