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 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 :: thesis: ( B = {} implies F $$ ((B \/ {.x.}),f) = F . ((F $$ (B,f)),(f . x)) )

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

end;

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