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

per cases ;
:: according to ORDINAL2:def 13

case Z1: Union f = {} ; :: thesis:

take the Element of dom f ; :: thesis:
thus the Element of dom f in dom f by Z0; :: thesis:
let c be ordinal number ; :: thesis:
assume ( the Element of dom f c= c & c in dom f ) ; :: thesis:
then f . c in rng f by FUNCT_1:def 5;
hence f . c = {} by Z1, ORDERS_1:91; :: thesis:

end;

case Union f <> {} ; :: thesis:

let b, c be ordinal number ; :: thesis:
assume A1: ( b in Union f & Union f in c ) ; :: thesis:
then consider x being set such that
A2: ( x in dom f & b in f . x ) by CARD_5:10;
reconsider x = x as Ordinal by A2;
take x ; :: thesis:
thus x in dom f by A2; :: thesis:
let E be Ordinal; :: thesis:
assume Z2: ( x c= E & E in dom f ) ; :: thesis:
then ( x = E or x c< E ) by XBOOLE_0:def 8;
then ( x = E or x in E ) by ORDINAL1:21;
then f . x c= f . E by Z2, ND;
hence b in f . E by A2; :: thesis:
f . E in rng f by Z2, FUNCT_1:def 5;
then f . E c= Union f by ZFMISC_1:92;
hence f . E in c by A1, ORDINAL1:22; :: thesis:

end;

end;