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_right_unity_wrt F holds
EqClass (RD,d) is_a_right_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_right_unity_wrt F holds
EqClass (RD,d) is_a_right_unity_wrt F /\/ RD

let d be Element of D; :: thesis: for F being BinOp of D,RD st d is_a_right_unity_wrt F holds
EqClass (RD,d) is_a_right_unity_wrt F /\/ RD

let F be BinOp of D,RD; :: thesis: ( d is_a_right_unity_wrt F implies EqClass (RD,d) is_a_right_unity_wrt F /\/ RD )
defpred S1[ Element of Class RD] means (F /\/ RD) . (\$1,(EqClass (RD,d))) = \$1;
assume A1: for a being Element of D holds F . (a,d) = a ; :: according to BINOP_1:def 17 :: thesis: EqClass (RD,d) is_a_right_unity_wrt F /\/ RD
A2: now :: thesis: for a being Element of D holds S1[ EqClass (RD,a)]
let a be Element of D; :: thesis: S1[ EqClass (RD,a)]
(F /\/ RD) . ((EqClass (RD,a)),(EqClass (RD,d))) = EqClass (RD,(F . (a,d))) by Th3
.= EqClass (RD,a) by A1 ;
hence S1[ EqClass (RD,a)] ; :: thesis: verum
end;
thus for c being Element of Class RD holds S1[c] from :: according to BINOP_1:def 17 :: thesis: verum