let Y, X be non empty set ; :: thesis: for F being BinOp of Y
for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds
for B1, B2 being Element of Fin X holds F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)
let F be BinOp of Y; :: thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds
for B1, B2 being Element of Fin X holds F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)
let f be Function of X,Y; :: thesis: ( F is idempotent & F is commutative & F is associative & F is having_a_unity implies for B1, B2 being Element of Fin X holds F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f) )
assume that
A1: ( F is idempotent & F is commutative & F is associative ) and
A2: F is having_a_unity ; :: thesis: for B1, B2 being Element of Fin X holds F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)
let B1, B2 be Element of Fin X; :: thesis: F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)

now

assume A3: ( B1 = {} or B2 = {} ) ; :: thesis: F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)
A4: {} = {}. X ;

per cases ( B2 = {} or B1 = {} ) by A3;

suppose A5: B2 = {} ; :: thesis: F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)

hence F $$ (B1 \/ B2),f = F . (F $$ B1,f),(the_unity_wrt F) by A2, Th23
.= F . (F $$ B1,f),(F $$ B2,f) by A1, A2, A4, A5, Th40 ;
:: thesis: verum

end;

suppose A6: B1 = {} ; :: thesis: F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)

hence F $$ (B1 \/ B2),f = F . (the_unity_wrt F),(F $$ B2,f) by A2, Th23
.= F . (F $$ B1,f),(F $$ B2,f) by A1, A2, A4, A6, Th40 ;
:: thesis: verum

end;

end;

end;

hence F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f) by A1, Th30; :: thesis: verum