let Y, X 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 A1: ( F is commutative & F is associative & 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 A2: 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, Th26
.= F $$ ({.x.} \/ B),f by A1, A2, Th30
.= F $$ B,f by A2, ZFMISC_1:46 ; :: thesis: verum