let A be set ; :: thesis: for D being non empty set
for o being BinOp of D st o is having_a_unity holds
( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity )
let D be non empty set ; :: thesis: for o being BinOp of D st o is having_a_unity holds
( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity )
let o be BinOp of D; :: thesis: ( o is having_a_unity implies ( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity ) )
given a being Element of D such that A1: a is_a_unity_wrt o ; :: according to SETWISEO:def 2 :: thesis: ( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity )
( a = the_unity_wrt o & A --> a is_a_unity_wrt (o,D) .: A ) by A1, Th9, BINOP_1:def 8;
hence the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) by BINOP_1:def 8; :: thesis: (o,D) .: A is having_a_unity
take A --> a ; :: according to SETWISEO:def 2 :: thesis: A --> a is_a_unity_wrt (o,D) .: A
thus A --> a is_a_unity_wrt (o,D) .: A by A1, Th9; :: thesis: verum