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;