let A be Cantor-normal-form Ordinal-Sequence; :: thesis: omega -exponent A is XFinSequence of sup (omega -exponent A)
now :: thesis: for y being object st y in rng (omega -exponent A) holds
y in sup (omega -exponent A)
let y be object ; :: thesis: ( y in rng (omega -exponent A) implies y in sup (omega -exponent A) )
assume y in rng (omega -exponent A) ; :: thesis: y in sup (omega -exponent A)
then y in sup (rng (omega -exponent A)) by ORDINAL2:19;
hence y in sup (omega -exponent A) by ORDINAL2:def 5; :: thesis: verum
end;
hence omega -exponent A is XFinSequence of sup (omega -exponent A) by TARSKI:def 3, RELAT_1:def 19; :: thesis: verum