let f be non-decreasing Ordinal-Sequence; :: thesis:
assume A1: not dom f is empty ; :: thesis:
set a0 = the Element of dom f;

per cases ;
:: according to ORDINAL2:def 9

case A2: Union f = 0 ; :: thesis:

take the Element of dom f ; :: thesis:
thus the Element of dom f in dom f by A1; :: thesis:
let c be Ordinal; :: thesis:
assume ( the Element of dom f c= c & c in dom f ) ; :: thesis:
then f . c in rng f by FUNCT_1:def 3;
hence f . c = 0 by A2, ORDERS_1:6; :: thesis:

end;

case Union f <> 0 ; :: thesis:

let b, c be Ordinal; :: thesis:
assume A3: ( b in Union f & Union f in c ) ; :: thesis:
then consider x being object such that
A4: ( x in dom f & b in f . x ) by CARD_5:2;
reconsider x = x as Ordinal by A4;
take x ; :: thesis:
thus x in dom f by A4; :: thesis:
let E be Ordinal; :: thesis:
assume A5: ( x c= E & E in dom f ) ; :: thesis:
then ( x = E or x c< E ) ;
then ( x = E or x in E ) by ORDINAL1:11;
then f . x c= f . E by A5, Def2;
hence b in f . E by A4; :: thesis:
f . E in rng f by A5, FUNCT_1:def 3;
then f . E c= Union f by ZFMISC_1:74;
hence f . E in c by A3, ORDINAL1:12; :: thesis:

end;

end;