let X, Y 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 and
A2: ( F is commutative & F is associative ) and
A3: 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 :: thesis: ( ( B1 = {} or B2 = {} ) implies F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) )

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

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

suppose A6: 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 A3, Th12
.= F . ((F $$ (B1,f)),(F $$ (B2,f))) by A2, A3, A4, A6, Th28 ;
:: thesis: verum

end;

suppose A7: 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 A3, Th12
.= F . ((F $$ (B1,f)),(F $$ (B2,f))) by A2, A3, A4, A7, Th28 ;
:: thesis: verum

end;

end;

end;

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