let D be non empty set ; :: thesis: for g being BinOp of D st g is having_a_unity holds
g "**" (<*> D) = the_unity_wrt g
let g be BinOp of D; :: thesis: ( g is having_a_unity implies g "**" (<*> D) = the_unity_wrt g )
A1: len (<*> D) = 0 ;
assume g is having_a_unity ; :: thesis: g "**" (<*> D) = the_unity_wrt g
hence g "**" (<*> D) = the_unity_wrt g by A1, Def1; :: thesis: verum