let f be Ordinal-Sequence; ( f = id a implies f is continuous )
assume A1:
f = id a
; f is continuous
let b be ordinal number ; ORDINAL2:def 13 for b1 being set holds
( not b in proj1 f or b = {} or not b is limit_ordinal or not b1 = f . b or b1 is_limes_of f | b )
let c be ordinal number ; ( not b in proj1 f or b = {} or not b is limit_ordinal or not c = f . b or c is_limes_of f | b )
assume A2:
( b in dom f & b <> {} & b is limit_ordinal & c = f . b )
; c is_limes_of f | b
set g = f | b;
A3:
( dom f = a & dom (id b) = b )
by A1, RELAT_1:45;
then A4:
c = b
by A1, A2, FUNCT_1:18;
b c= a
by A2, A3, ORDINAL1:def 2;
then A5:
f | b = id b
by A1, FUNCT_3:1;
per cases
( c = {} or c <> {} )
;
ORDINAL2:def 9case
c <> {}
;
for b1, b2 being set holds
( not b1 in c or not c in b2 or ex b3 being set st
( b3 in proj1 (f | b) & ( for b4 being set holds
( not b3 c= b4 or not b4 in proj1 (f | b) or ( b1 in (f | b) . b4 & (f | b) . b4 in b2 ) ) ) ) )let B,
C be
Ordinal;
( not B in c or not c in C or ex b1 being set st
( b1 in proj1 (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in proj1 (f | b) or ( B in (f | b) . b2 & (f | b) . b2 in C ) ) ) ) )assume B1:
(
B in c &
c in C )
;
ex b1 being set st
( b1 in proj1 (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in proj1 (f | b) or ( B in (f | b) . b2 & (f | b) . b2 in C ) ) ) )take D =
succ B;
( D in proj1 (f | b) & ( for b1 being set holds
( not D c= b1 or not b1 in proj1 (f | b) or ( B in (f | b) . b1 & (f | b) . b1 in C ) ) ) )thus
D in dom (f | b)
by A2, A3, A4, A5, B1, ORDINAL1:28;
for b1 being set holds
( not D c= b1 or not b1 in proj1 (f | b) or ( B in (f | b) . b1 & (f | b) . b1 in C ) )let E be
Ordinal;
( not D c= E or not E in proj1 (f | b) or ( B in (f | b) . E & (f | b) . E in C ) )assume B3:
(
D c= E &
E in dom (f | b) )
;
( B in (f | b) . E & (f | b) . E in C )then
(f | b) . E = E
by A3, A5, FUNCT_1:18;
hence
(
B in (f | b) . E &
(f | b) . E in C )
by A3, A4, A5, B1, B3, ORDINAL1:10, ORDINAL1:21;
verum end;