let X, Y be non empty set ; for F being BinOp of Y
for f being Function of X,Y st F is commutative & F is associative holds
for b being Element of X holds F $$ ({.b.},f) = f . b
let F be BinOp of Y; for f being Function of X,Y st F is commutative & F is associative holds
for b being Element of X holds F $$ ({.b.},f) = f . b
let f be Function of X,Y; ( F is commutative & F is associative implies for b being Element of X holds F $$ ({.b.},f) = f . b )
assume A1:
( F is commutative & F is associative )
; for b being Element of X holds F $$ ({.b.},f) = f . b
let b be Element of X; F $$ ({.b.},f) = f . b
ex G being Function of (Fin X),Y st
( F $$ ({.b.},f) = G . {b} & ( for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= {b} & B9 <> {} holds
for x being Element of X st x in {b} \ B9 holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) )
by A1, Def3;
hence
F $$ ({.b.},f) = f . b
; verum