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 & F is commutative & F is associative ) and
A2: 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

assume B = {} ; :: thesis: F $$ (f .: B),g = F $$ B,(g * f)
then ( B = {}. X & f .: B = {}. Y ) by RELAT_1:149;
then ( F $$ (f .: B),g = the_unity_wrt F & F $$ B,(g * f) = the_unity_wrt F ) by A1, A2, Th40;
hence F $$ (f .: B),g = F $$ B,(g * f) ; :: thesis: verum

end;

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