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