set f = isoR (x,o);
A1: the carrier of (ExField (x,o)) = carr (x,o) by Def8;
A2: rng (isoR (x,o)) c= the carrier of (ExField (x,o)) by RELAT_1:def 19;
now :: thesis: for u being object st u in the carrier of (ExField (x,o)) holds
u in rng (isoR (x,o))
let u be object ; :: thesis: ( u in the carrier of (ExField (x,o)) implies b1 in rng (isoR (x,o)) )
assume A3: u in the carrier of (ExField (x,o)) ; :: thesis: b1 in rng (isoR (x,o))
per cases ( o = u or o <> u ) ;
suppose o = u ; :: thesis: b1 in rng (isoR (x,o))
then A4: (isoR (x,o)) . x = u by Def9;
[#] F = dom (isoR (x,o)) by FUNCT_2:def 1;
hence u in rng (isoR (x,o)) by A4, FUNCT_1:def 3; :: thesis: verum
end;
suppose o <> u ; :: thesis: b1 in rng (isoR (x,o))
then not u in {o} by TARSKI:def 1;
then A5: u in ([#] F) \ {x} by A3, A1, XBOOLE_0:def 3;
then reconsider a = u as Element of F ;
not u in {x} by A5, XBOOLE_0:def 5;
then x <> u by TARSKI:def 1;
then A6: (isoR (x,o)) . a = a by Def9;
[#] F = dom (isoR (x,o)) by FUNCT_2:def 1;
hence u in rng (isoR (x,o)) by A6, FUNCT_1:def 3; :: thesis: verum
end;
end;
end;
hence isoR (x,o) is onto by A2, TARSKI:2; :: thesis: verum