let A, X, Y be non empty set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f))
let g be Function of Y,A; :: thesis: F $$ ((f .: B),g) = F $$ (B,(g * f))

now :: thesis: ( B = {} implies F $$ ((f .: B),g) = F $$ (B,(g * f)) )

assume A4: B = {} ; :: thesis: 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; :: thesis: verum

end;

hence F $$ ((f .: B),g) = F $$ (B,(g * f)) by A1, A2, Th26; :: thesis: verum