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 A1: ( F is idempotent & 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 A2: F is having_a_unity ; :: thesis: for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
A3: {} = {}. X ;
let x be Element of X; :: thesis: F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)

now

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

end;

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