let X, Y be non empty set ; :: thesis: for F being BinOp of Y
for B being Element of Fin X
for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for x being Element of X st x in B holds
F . ((f . x),(F $$ (B,f))) = F $$ (B,f)
let F be BinOp of Y; :: thesis: for B being Element of Fin X
for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for x being Element of X st x in B holds
F . ((f . x),(F $$ (B,f))) = F $$ (B,f)
let B be Element of Fin X; :: thesis: for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for x being Element of X st x in B holds
F . ((f . x),(F $$ (B,f))) = F $$ (B,f)
let f be Function of X,Y; :: thesis: ( F is commutative & F is associative & F is idempotent implies for x being Element of X st x in B holds
F . ((f . x),(F $$ (B,f))) = F $$ (B,f) )
assume that
A1: ( F is commutative & F is associative ) and
A2: F is idempotent ; :: thesis: for x being Element of X st x in B holds
F . ((f . x),(F $$ (B,f))) = F $$ (B,f)
let x be Element of X; :: thesis: ( x in B implies F . ((f . x),(F $$ (B,f))) = F $$ (B,f) )
assume A3: x in B ; :: thesis: F . ((f . x),(F $$ (B,f))) = F $$ (B,f)
thus F . ((f . x),(F $$ (B,f))) = F . ((F $$ ({.x.},f)),(F $$ (B,f))) by A1, Th14
.= F $$ (({.x.} \/ B),f) by A1, A2, A3, Th18
.= F $$ (B,f) by A3, ZFMISC_1:40 ; :: thesis: verum