set F = the Field;
deffunc H₁( object ) -> Field = the Field;
consider f being Function such that
A: ( dom f = NAT & ( for x being object st x in NAT holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
reconsider f = f as sequence by A, ds;
take f ; :: thesis: f is Field-yielding

now :: thesis: for x being object st x in rng f holds
x is Field

let x be object ; :: thesis: ( x in rng f implies x is Field )
assume x in rng f ; :: thesis: x is Field
then consider o being object such that
B: ( o in dom f & f . o = x ) by FUNCT_1:def 3;
thus x is Field by A, B; :: thesis: verum

end;

hence f is Field-yielding ; :: thesis: verum