let f be Function; :: thesis: ( f is Ordinal-yielding iff for x being object st x in dom f holds
f . x is Ordinal )
hereby :: thesis: ( ( for x being object st x in dom f holds
f . x is Ordinal ) implies f is Ordinal-yielding )
assume f is Ordinal-yielding ; :: thesis: for x being object st x in dom f holds
f . x is Ordinal
then consider A being Ordinal such that
A1: rng f c= A by ORDINAL2:def 4;
let x be object ; :: thesis: ( x in dom f implies f . x is Ordinal )
assume x in dom f ; :: thesis: f . x is Ordinal
then f . x in rng f by FUNCT_1:3;
hence f . x is Ordinal by A1; :: thesis: verum
end;
assume A2: for x being object st x in dom f holds
f . x is Ordinal ; :: thesis: f is Ordinal-yielding
now :: thesis: ex A being Ordinal st rng f c= A
reconsider A = sup (rng f) as Ordinal ;
take A = A; :: thesis: rng f c= A
now :: thesis: for y being object st y in rng f holds
y in A
let y be object ; :: thesis: ( y in rng f implies y in A )
assume A3: y in rng f ; :: thesis: y in A
then consider x being object such that
A4: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
y is Ordinal by A2, A4;
then A5: y in On (rng f) by A3, ORDINAL1:def 9;
On (rng f) c= A by ORDINAL2:def 3;
hence y in A by A5; :: thesis: verum
end;
hence rng f c= A by TARSKI:def 3; :: thesis: verum
end;
hence f is Ordinal-yielding by ORDINAL2:def 4; :: thesis: verum