let Y, X 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, Th30
.= F $$ C,f by A3, XBOOLE_1:12 ;
:: thesis: verum