let Y, X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: for b being Element of X holds F $$ {.b.},f = f . b
let b be Element of X; :: thesis: 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 B' being Element of Fin X st B' c= {b} & B' <> {} holds
for x being Element of X st x in {b} \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) by A1, Def3;
hence F $$ {.b.},f = f . b ; :: thesis: verum