let X, Y be non empty set ; :: thesis: for F being BinOp of Y
for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for B, C being Element of Fin X st B <> {} & B c= C holds
F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ (C,f)
let F be BinOp of Y; :: thesis: for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for B, C being Element of Fin X st B <> {} & B c= C holds
F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ (C,f)
let f be Function of X,Y; :: thesis: ( F is commutative & F is associative & F is idempotent implies for B, C being Element of Fin X st B <> {} & B c= C holds
F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ (C,f) )
assume A1: ( F is commutative & F is associative & F is idempotent ) ; :: thesis: for B, C being Element of Fin X st B <> {} & B c= C holds
F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ (C,f)
let B, C be Element of Fin X; :: thesis: ( B <> {} & B c= C implies F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ (C,f) )
assume that
A2: B <> {} and
A3: B c= C ; :: thesis: F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ (C,f)
C <> {} by A2, A3;
hence F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ ((B \/ C),f) by A1, A2, Th18
.= F $$ (C,f) by A3, XBOOLE_1:12 ;
:: thesis: verum