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) . ($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:

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

end;