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 :: 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)))

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, Th23
.= F $$ ({.y.},(G [:] (g,(F $$ ({.x.},f))))) by A1, Th24
.= F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g))) by A2, FUNCOP_1:64 ; :: 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