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_left_unity_wrt F holds

EqClass (RD,d) is_a_left_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_left_unity_wrt F holds

EqClass (RD,d) is_a_left_unity_wrt F /\/ RD

let d be Element of D; :: thesis: for F being BinOp of D,RD st d is_a_left_unity_wrt F holds

EqClass (RD,d) is_a_left_unity_wrt F /\/ RD

let F be BinOp of D,RD; :: thesis: ( d is_a_left_unity_wrt F implies EqClass (RD,d) is_a_left_unity_wrt F /\/ RD )

defpred S_{1}[ 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: EqClass (RD,d) is_a_left_unity_wrt F /\/ RD

_{1}[c]
from FILTER_1:sch 1(A2); :: according to BINOP_1:def 16 :: thesis: verum

for d being Element of D

for F being BinOp of D,RD st d is_a_left_unity_wrt F holds

EqClass (RD,d) is_a_left_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_left_unity_wrt F holds

EqClass (RD,d) is_a_left_unity_wrt F /\/ RD

let d be Element of D; :: thesis: for F being BinOp of D,RD st d is_a_left_unity_wrt F holds

EqClass (RD,d) is_a_left_unity_wrt F /\/ RD

let F be BinOp of D,RD; :: thesis: ( d is_a_left_unity_wrt F implies EqClass (RD,d) is_a_left_unity_wrt F /\/ RD )

defpred S

assume A1: for a being Element of D holds F . (d,a) = a ; :: according to BINOP_1:def 16 :: thesis: EqClass (RD,d) is_a_left_unity_wrt F /\/ RD

A2: now :: thesis: for a being Element of D holds S_{1}[ EqClass (RD,a)]

thus
for c being Element of Class RD holds Slet a be Element of D; :: thesis: S_{1}[ EqClass (RD,a)]

(F /\/ RD) . ((EqClass (RD,d)),(EqClass (RD,a))) = Class (RD,(F . (d,a))) by Th3

.= EqClass (RD,a) by A1 ;

hence S_{1}[ EqClass (RD,a)]
; :: thesis: verum

end;(F /\/ RD) . ((EqClass (RD,d)),(EqClass (RD,a))) = Class (RD,(F . (d,a))) by Th3

.= EqClass (RD,a) by A1 ;

hence S