let Y, X be non empty set ; :: thesis: for F being BinOp of Y st F is commutative & F is associative & F is having_a_unity holds
for f being Function of X,Y holds F $$ ({}. X),f = the_unity_wrt F
let F be BinOp of Y; :: thesis: ( F is commutative & F is associative & F is having_a_unity implies for f being Function of X,Y holds F $$ ({}. X),f = the_unity_wrt F )
assume that
A1: ( F is commutative & F is associative ) and
A2: F is having_a_unity ; :: thesis: for f being Function of X,Y holds F $$ ({}. X),f = the_unity_wrt F
let f be Function of X,Y; :: thesis: F $$ ({}. X),f = the_unity_wrt F
A3: ( the_unity_wrt F is_a_unity_wrt F & {} = {}. X ) by A2, Th22;
ex G being Function of (Fin X),Y st
( F $$ ({}. X),f = G . ({}. X) & ( 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= {}. X & B' <> {} holds
for x being Element of X st x in ({}. X) \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) by A1, A2, Def3;
hence F $$ ({}. X),f = the_unity_wrt F by A3; :: thesis: verum