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 )
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
defpred S₁[ Element of Class RD] means (F /\/ RD) . $1,(EqClass RD,d) = $1;

A2: now

let a be Element of D; :: thesis: S₁[ EqClass RD,a]
thus S₁[ EqClass RD,a] :: thesis: verum

proof

thus (F /\/ RD) . (EqClass RD,a),(EqClass RD,d) = EqClass RD,(F . a,d) by Th3
.= EqClass RD,a by A1 ; :: thesis: verum

end;

end;

thus for c being Element of Class RD holds S₁[c] from FILTER_1:sch 1(A2); :: according to BINOP_1:def 17 :: thesis: verum