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 set ; :: 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 set such that
A2: x in the carrier of R and
A3: A = Class (EqRel R,{(0. R)}),x by EQREL_1:def 5;
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 set ; :: 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:27;
then a - x in {(0. R)} by Def5;
then a - x = 0. R by TARSKI:def 1;
then a = x by RLVECT_1:35;
hence a in {x} by TARSKI:def 1; :: thesis: verum

end;

let a be set ; :: 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:28;
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:27; :: 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 5; :: thesis: verum

end;

let A be set ; :: 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 set such that
A7: w in dom (singleton the carrier of R) and
A8: (singleton the carrier of R) . w = A by FUNCT_1:def 5;
(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 5; :: thesis: verum