let X, Y 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 A1: ( F is commutative & F is associative & 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
( the_unity_wrt F is_a_unity_wrt F & 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 B9 being Element of Fin X st B9 c= {}. X & B9 <> {} holds
for x being Element of X st x in ({}. X) \ B9 holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) by A1, Def3, Th11;
hence F $$ (({}. X),f) = the_unity_wrt F ; :: thesis: verum