deffunc H₁( object ) -> set = b -exponent (A . $1);
consider f being Function such that
A1: ( dom f = dom A & ( for a being object st a in dom A holds
f . a = H₁(a) ) ) from FUNCT_1:sch 3();
reconsider f = f as Sequence by A1, ORDINAL1:31;

now :: thesis: ex c being Ordinal st rng f c= sup (rng f)

reconsider c = sup (rng f) as Ordinal ;
take c = c; :: thesis: rng f c= sup (rng f)

now :: thesis: for y being object st y in rng f holds
y in sup (rng f)

let y be object ; :: thesis: ( y in rng f implies y in sup (rng f) )
assume A2: y in rng f ; :: thesis: y in sup (rng f)
then consider x being object such that
A3: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
f . x = b -exponent (A . x) by A1, A3;
hence y in sup (rng f) by A2, A3, ORDINAL2:19; :: thesis: verum

end;

hence rng f c= sup (rng f) by TARSKI:def 3; :: thesis: verum

end;

then reconsider f = f as Ordinal-Sequence by ORDINAL2:def 4;
take f ; :: thesis: ( dom f = dom A & ( for a being object st a in dom A holds
f . a = b -exponent (A . a) ) )
thus ( dom f = dom A & ( for a being object st a in dom A holds
f . a = b -exponent (A . a) ) ) by A1; :: thesis: verum