now :: thesis: for y being object st y in rng (omega -leading_coeff A) holds
y in NAT
let y be object ; :: thesis: ( y in rng (omega -leading_coeff A) implies y in NAT )
assume y in rng (omega -leading_coeff A) ; :: thesis: y in NAT
then consider x being object such that
A1: ( x in dom (omega -leading_coeff A) & (omega -leading_coeff A) . x = y ) by FUNCT_1:def 3;
thus y in NAT by A1, ORDINAL1:def 12; :: thesis: verum
end;
hence omega -leading_coeff A is natural-valued by TARSKI:def 3, VALUED_0:def 6; :: thesis: omega -leading_coeff A is non-empty
now :: thesis: for x being object st x in dom (omega -leading_coeff A) holds
not (omega -leading_coeff A) . x is empty
let x be object ; :: thesis: ( x in dom (omega -leading_coeff A) implies not (omega -leading_coeff A) . x is empty )
assume x in dom (omega -leading_coeff A) ; :: thesis: not (omega -leading_coeff A) . x is empty
then A2: x in dom A by Def3;
then A3: A . x is Cantor-component by ORDINAL5:def 11;
(omega -leading_coeff A) . x = omega -leading_coeff (A . x) by A2, Def3;
hence not (omega -leading_coeff A) . x is empty by A3; :: thesis: verum
end;
hence omega -leading_coeff A is non-empty by FUNCT_1:def 9; :: thesis: verum