per cases ( a in dom A or not a in dom A ) ;

suppose A1: a in dom A ; :: thesis: (omega -leading_coeff A) . a is natural

then A2: (omega -leading_coeff A) . a = omega -leading_coeff (A . a) by Def3;
A . a is Cantor-component by A1, ORDINAL5:def 11;
hence (omega -leading_coeff A) . a is natural by A2; :: thesis: verum

end;

suppose not a in dom A ; :: thesis: (omega -leading_coeff A) . a is natural

then not a in dom (omega -leading_coeff A) by Def3;
hence (omega -leading_coeff A) . a is natural by FUNCT_1:def 2; :: thesis: verum

end;

end;