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
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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: 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, 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 ; :: thesis: verum