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;

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))

hence
isoR (x,o) is onto
by A2, TARSKI:2; :: thesis: verumu in rng (isoR (x,o))

let u be object ; :: thesis: ( u in the carrier of (ExField (x,o)) implies b_{1} in rng (isoR (x,o)) )

assume A3: u in the carrier of (ExField (x,o)) ; :: thesis: b_{1} in rng (isoR (x,o))

end;assume A3: u in the carrier of (ExField (x,o)) ; :: thesis: b

per cases
( o = u or o <> u )
;

end;

suppose
o = u
; :: thesis: b_{1} 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;[#] 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

suppose
o <> u
; :: thesis: b_{1} 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;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