let D be non empty set ; 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 having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let I, J be 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 having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let F, G be 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 having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let f be 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 having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let g be Function of J,D; for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let X be Element of Fin I; for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let Y be Element of Fin J; ( F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative implies F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g))) )
assume that
A1:
( F is having_a_unity & F is commutative & F is associative )
and
A2:
( F is having_an_inverseOp & G is_distributive_wrt F )
and
A3:
G is commutative
; 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, A3, Th23
.=
F $$ (Y,(G [:] (g,(F $$ (X,f)))))
by A1, A2, Th26
.=
F $$ (Y,(G [;] ((F $$ (X,f)),g)))
by A3, FUNCOP_1:64
; verum