let A be Ordinal; :: thesis: for S being Sequence st dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) holds
for O being Ordinal st O in succ A holds
S . O = No_Ordinal_op O
let S be Sequence; :: thesis: ( dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) implies for O being Ordinal st O in succ A holds
S . O = No_Ordinal_op O )
assume that
A1: dom S = succ A and
A2: ( ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) ; :: thesis: for O being Ordinal st O in succ A holds
S . O = No_Ordinal_op O
let O be Ordinal; :: thesis: ( O in succ A implies S . O = No_Ordinal_op O )
assume A3: O in succ A ; :: thesis: S . O = No_Ordinal_op O
consider So being Sequence such that
A4: ( No_Ordinal_op O = So . O & dom So = succ O ) and
A5: ( ( for B being Ordinal st succ B in succ O holds
So . (succ B) = [{(So . B)},{}] ) & ( for B being Ordinal st B in succ O & B is limit_ordinal holds
So . B = [(rng (So | B)),{}] ) ) by Def11;
defpred S₁[ Ordinal] means ( $1 c= O implies So . $1 = S . $1 );
A6: for B being Ordinal st ( for C being Ordinal st C in B holds
S₁[C] ) holds
S₁[B]

proof

let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
assume A7: for C being Ordinal st C in B holds
S₁[C] ; :: thesis: S₁[B]
assume A8: B c= O ; :: thesis: So . B = S . B
then A9: B in succ O by ORDINAL1:22;
A10: B in succ A by A3, A8, ORDINAL1:12;

per cases ( not B is limit_ordinal or B is limit_ordinal ) ;

suppose not B is limit_ordinal ; :: thesis: So . B = S . B

then consider C being Ordinal such that
A11: B = succ C by ORDINAL1:29;
A12: C in B by A11, ORDINAL1:21;
S . C = So . C by A8, A12, A7, ORDINAL1:def 2;
then So . B = [{(S . C)},{}] by A5, A8, ORDINAL1:22, A11;
hence So . B = S . B by A3, A8, ORDINAL1:12, A2, A11; :: thesis: verum

end;

suppose B is limit_ordinal ; :: thesis: So . B = S . B

then A13: ( S . B = [(rng (S | B)),{}] & So . B = [(rng (So | B)),{}] ) by A2, A5, A8, ORDINAL1:22, A3, ORDINAL1:12;
A14: ( dom (S | B) = B & dom (So | B) = B ) by A4, A1, A9, ORDINAL1:def 2, RELAT_1:62, A10;
for x being object st x in B holds
(So | B) . x = (S | B) . x

proof

let x be object ; :: thesis: ( x in B implies (So | B) . x = (S | B) . x )
assume A15: x in B ; :: thesis: (So | B) . x = (S | B) . x
reconsider x = x as Ordinal by A15;
(So | B) . x = So . x by A15, FUNCT_1:49
.= S . x by A15, A7, A8, ORDINAL1:def 2 ;
hence (So | B) . x = (S | B) . x by A15, FUNCT_1:49; :: thesis: verum

end;

hence So . B = S . B by A13, A14, FUNCT_1:2; :: thesis: verum

end;

end;

end;

for B being Ordinal holds S₁[B] from ORDINAL1:sch 2(A6);
hence S . O = No_Ordinal_op O by A4; :: thesis: verum