let f be Ordinal-Sequence; :: thesis: ( f = id a implies f is continuous )
assume A1: f = id a ; :: thesis: f is continuous
let b be Ordinal; :: according to ORDINAL2:def 13 :: thesis: for b1 being set holds
( not b in dom f or b = 0 or not b is limit_ordinal or not b1 = f . b or b1 is_limes_of f | b )
let c be Ordinal; :: thesis: ( not b in dom f or b = 0 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 <> 0 & b is limit_ordinal & c = f . b ) ; :: thesis: c is_limes_of f | b
set g = f | b;
A3: ( dom f = a & dom (id b) = b ) by A1;
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 = 0 or c <> 0 ) ;
:: according to ORDINAL2:def 9
case c = 0 ; :: thesis: ex b1 being set st
( b1 in dom (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (f | b) or (f | b) . b2 = 0 ) ) )
hence ex b1 being set st
( b1 in dom (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (f | b) or (f | b) . b2 = 0 ) ) ) by A2, A1, FUNCT_1:18; :: thesis: verum
end;
case c <> 0 ; :: thesis: for b1, b2 being set holds
( not b1 in c or not c in b2 or ex b3 being set st
( b3 in dom (f | b) & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom (f | b) or ( b1 in (f | b) . b4 & (f | b) . b4 in b2 ) ) ) ) )
let B, C be Ordinal; :: thesis: ( not B in c or not c in C or ex b1 being set st
( b1 in dom (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (f | b) or ( B in (f | b) . b2 & (f | b) . b2 in C ) ) ) ) )
assume A6: ( B in c & c in C ) ; :: thesis: ex b1 being set st
( b1 in dom (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (f | b) or ( B in (f | b) . b2 & (f | b) . b2 in C ) ) ) )
take D = succ B; :: thesis: ( D in dom (f | b) & ( for b1 being set holds
( not D c= b1 or not b1 in dom (f | b) or ( B in (f | b) . b1 & (f | b) . b1 in C ) ) ) )
thus D in dom (f | b) by A2, A4, A5, A6, ORDINAL1:28; :: thesis: for b1 being set holds
( not D c= b1 or not b1 in dom (f | b) or ( B in (f | b) . b1 & (f | b) . b1 in C ) )
let E be Ordinal; :: thesis: ( not D c= E or not E in dom (f | b) or ( B in (f | b) . E & (f | b) . E in C ) )
assume A7: ( D c= E & E in dom (f | b) ) ; :: thesis: ( B in (f | b) . E & (f | b) . E in C )
then (f | b) . E = E by A5, FUNCT_1:18;
hence ( B in (f | b) . E & (f | b) . E in C ) by A4, A5, A6, A7, ORDINAL1:10, ORDINAL1:21; :: thesis: verum
end;
end;