let R be Ring; :: thesis: Class (EqRel (R,{(0. R)})) = rng (singleton the carrier of R)
set E = EqRel (R,{(0. R)});
set f = singleton the carrier of R;
A1: dom (singleton the carrier of R) = the carrier of R by FUNCT_2:def 1;
thus Class (EqRel (R,{(0. R)})) c= rng (singleton the carrier of R) :: according to XBOOLE_0:def 10 :: thesis: rng (singleton the carrier of R) c= Class (EqRel (R,{(0. R)}))

proof

let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in Class (EqRel (R,{(0. R)})) or A in rng (singleton the carrier of R) )
assume A in Class (EqRel (R,{(0. R)})) ; :: thesis: A in rng (singleton the carrier of R)
then consider x being object such that
A2: x in the carrier of R and
A3: A = Class ((EqRel (R,{(0. R)})),x) by EQREL_1:def 3;
reconsider x = x as Element of R by A2;
A4: Class ((EqRel (R,{(0. R)})),x) = {x}

proof

thus Class ((EqRel (R,{(0. R)})),x) c= {x} :: according to XBOOLE_0:def 10 :: thesis: {x} c= Class ((EqRel (R,{(0. R)})),x)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Class ((EqRel (R,{(0. R)})),x) or a in {x} )
assume A5: a in Class ((EqRel (R,{(0. R)})),x) ; :: thesis: a in {x}
then reconsider a = a as Element of R ;
[a,x] in EqRel (R,{(0. R)}) by A5, EQREL_1:19;
then a - x in {(0. R)} by Def5;
then a - x = 0. R by TARSKI:def 1;
then a = x by RLVECT_1:21;
hence a in {x} by TARSKI:def 1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} or a in Class ((EqRel (R,{(0. R)})),x) )
x - x = 0. R by RLVECT_1:15;
then A6: x - x in {(0. R)} by TARSKI:def 1;
assume a in {x} ; :: thesis: a in Class ((EqRel (R,{(0. R)})),x)
then a = x by TARSKI:def 1;
then [a,x] in EqRel (R,{(0. R)}) by A6, Def5;
hence a in Class ((EqRel (R,{(0. R)})),x) by EQREL_1:19; :: thesis: verum

end;

(singleton the carrier of R) . x = {x} by SETWISEO:def 6;
hence A in rng (singleton the carrier of R) by A1, A3, A4, FUNCT_1:def 3; :: thesis: verum

end;

let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in rng (singleton the carrier of R) or A in Class (EqRel (R,{(0. R)})) )
assume A in rng (singleton the carrier of R) ; :: thesis: A in Class (EqRel (R,{(0. R)}))
then consider w being object such that
A7: w in dom (singleton the carrier of R) and
A8: (singleton the carrier of R) . w = A by FUNCT_1:def 3;
(singleton the carrier of R) . w = {w} by A7, SETWISEO:def 6
.= Class ((EqRel (R,{(0. R)})),w) by A7, Th9 ;
hence A in Class (EqRel (R,{(0. R)})) by A7, A8, EQREL_1:def 3; :: thesis: verum