let f be non-decreasing Ordinal-Sequence; :: thesis: ( not dom f is empty implies Union f is_limes_of f )
assume A1: not dom f is empty ; :: thesis: Union f is_limes_of f
set a0 = the Element of dom f;
per cases ( Union f = 0 or Union f <> 0 ) ;
:: according to ORDINAL2:def 9
case A2: Union f = 0 ; :: thesis: ex b1 being set st
( b1 in dom f & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom f or f . b2 = 0 ) ) )
take the Element of dom f ; :: thesis: ( the Element of dom f in dom f & ( for b1 being set holds
( not the Element of dom f c= b1 or not b1 in dom f or f . b1 = 0 ) ) )
thus the Element of dom f in dom f by A1; :: thesis: for b1 being set holds
( not the Element of dom f c= b1 or not b1 in dom f or f . b1 = 0 )
let c be Ordinal; :: thesis: ( not the Element of dom f c= c or not c in dom f or f . c = 0 )
assume ( the Element of dom f c= c & c in dom f ) ; :: thesis: f . c = 0
then f . c in rng f by FUNCT_1:def 3;
hence f . c = 0 by A2, ORDERS_1:6; :: thesis: verum
end;
case Union f <> 0 ; :: thesis: for b1, b2 being set holds
( not b1 in Union f or not Union f in b2 or ex b3 being set st
( b3 in dom f & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom f or ( b1 in f . b4 & f . b4 in b2 ) ) ) ) )
let b, c be Ordinal; :: thesis: ( not b in Union f or not Union f in c or ex b1 being set st
( b1 in dom f & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom f or ( b in f . b2 & f . b2 in c ) ) ) ) )
assume A3: ( b in Union f & Union f in c ) ; :: thesis: ex b1 being set st
( b1 in dom f & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom f or ( b in f . b2 & f . b2 in c ) ) ) )
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: ( x in dom f & ( for b1 being set holds
( not x c= b1 or not b1 in dom f or ( b in f . b1 & f . b1 in c ) ) ) )
thus x in dom f by A4; :: thesis: for b1 being set holds
( not x c= b1 or not b1 in dom f or ( b in f . b1 & f . b1 in c ) )
let E be Ordinal; :: thesis: ( not x c= E or not E in dom f or ( b in f . E & f . E in c ) )
assume A5: ( x c= E & E in dom f ) ; :: thesis: ( b in f . E & f . E in c )
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 c
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: verum
end;
end;