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 & 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, A2, Th25
.= F $$ Y,(G [:] g,(F $$ X,f)) by A1, A2, Th28
.= F $$ Y,(G [;] (F $$ X,f),g) by A2, FUNCOP_1:79 ; :: thesis: verum