let D be non empty set ; :: thesis:
let RD be Equivalence_Relation of D; :: thesis:
let d be Element of D; :: thesis:
let F be BinOp of D,RD; :: thesis:
defpred S₁[ Element of Class RD] means (F /\/ RD) . (EqClass RD,d),$1 = $1;
assume A1: for a being Element of D holds F . d,a = a ; :: according to BINOP_1:def 16 :: thesis:

let a be Element of D; :: thesis:
(F /\/ RD) . (EqClass RD,d),(EqClass RD,a) = Class RD,(F . d,a) by Th3
.= EqClass RD,a by A1 ;
hence S₁[ EqClass RD,a] ; :: thesis:

end;