let A, X, Y be non empty set ; for F being BinOp of A st F is idempotent & F is commutative & F is associative & F is having_a_unity holds
for B being Element of Fin X
for f being Function of X,Y
for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f))
let F be BinOp of A; ( F is idempotent & F is commutative & F is associative & F is having_a_unity implies for B being Element of Fin X
for f being Function of X,Y
for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f)) )
assume that
A1:
F is idempotent
and
A2:
( F is commutative & F is associative )
and
A3:
F is having_a_unity
; for B being Element of Fin X
for f being Function of X,Y
for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f))
let B be Element of Fin X; for f being Function of X,Y
for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f))
let f be Function of X,Y; for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f))
let g be Function of Y,A; F $$ ((f .: B),g) = F $$ (B,(g * f))
now ( B = {} implies F $$ ((f .: B),g) = F $$ (B,(g * f)) )assume A4:
B = {}
;
F $$ ((f .: B),g) = F $$ (B,(g * f))then
f .: B = {}. Y
;
then A5:
F $$ (
(f .: B),
g)
= the_unity_wrt F
by A2, A3, Th28;
B = {}. X
by A4;
hence
F $$ (
(f .: B),
g)
= F $$ (
B,
(g * f))
by A2, A3, A5, Th28;
verum end;
hence
F $$ ((f .: B),g) = F $$ (B,(g * f))
by A1, A2, Th26; verum