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;

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;

then reconsider f = f as Field-yielding sequence by defFy;
take f ; :: thesis: f is ascending

now :: thesis: for i being Element of NAT holds f . (i + 1) is FieldExtension of f . i

let i be Element of NAT ; :: thesis: f . (i + 1) is FieldExtension of f . i
( f . i = the Field & f . (i + 1) = the Field ) by A;
hence f . (i + 1) is FieldExtension of f . i by FIELD_4:6; :: thesis: verum

end;

hence f is ascending ; :: thesis: verum