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;