let D be non empty set ; :: thesis: for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_unity_wrt F holds
EqClass (RD,d) is_a_unity_wrt F /\/ RD
let RD be Equivalence_Relation of D; :: thesis: for d being Element of D
for F being BinOp of D,RD st d is_a_unity_wrt F holds
EqClass (RD,d) is_a_unity_wrt F /\/ RD
let d be Element of D; :: thesis: for F being BinOp of D,RD st d is_a_unity_wrt F holds
EqClass (RD,d) is_a_unity_wrt F /\/ RD
let F be BinOp of D,RD; :: thesis: ( d is_a_unity_wrt F implies EqClass (RD,d) is_a_unity_wrt F /\/ RD )
assume that
A1: d is_a_left_unity_wrt F and
A2: d is_a_right_unity_wrt F ; :: according to BINOP_1:def 7 :: thesis: EqClass (RD,d) is_a_unity_wrt F /\/ RD
thus ( EqClass (RD,d) is_a_left_unity_wrt F /\/ RD & EqClass (RD,d) is_a_right_unity_wrt F /\/ RD ) by A1, A2, Th6, Th7; :: according to BINOP_1:def 7 :: thesis: verum