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 idempotent & F is commutative & F is associative & F is having_a_unity holds
for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
let F be BinOp of Y; :: thesis: for B being Element of Fin X
for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds
for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
let B be Element of Fin X; :: thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds
for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
let f be Function of X,Y; :: thesis: ( F is idempotent & F is commutative & F is associative & F is having_a_unity implies for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x) )
assume that
A1: F is idempotent and
A2: ( F is commutative & F is associative ) ; :: thesis: ( not F is having_a_unity or for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x) )
assume A3: F is having_a_unity ; :: thesis: for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
let x be Element of X; :: thesis: F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
A4: {} = {}. X ;

now

assume A5: B = {} ; :: thesis: F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
hence F $$ (B \/ {.x.}),f = f . x by A2, Th26
.= F . (the_unity_wrt F),(f . x) by A3, Th23
.= F . (F $$ B,f),(f . x) by A2, A3, A4, A5, Th40 ;
:: thesis: verum

end;

hence F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x) by A1, A2, Th29; :: thesis: verum