let X, Y be non empty set ; 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; 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; ( 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
; 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; F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
now ( ( B1 = {} or B2 = {} ) implies F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) )A4:
{} = {}. X
;
assume A5:
(
B1 = {} or
B2 = {} )
;
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))per cases
( B2 = {} or B1 = {} )
by A5;
suppose A6:
B2 = {}
;
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
;
verum end; suppose A7:
B1 = {}
;
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
;
verum end; end; end;
hence
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
by A1, A2, Th18; verum