let A be Ordinal; :: thesis: No_Ordinal_op (succ A) = [{(No_Ordinal_op A)},{}]
set B = succ A;
consider S being Sequence such that
A1: ( No_Ordinal_op (succ A) = S . (succ A) & dom S = succ (succ A) ) and
A2: ( ( for O being Ordinal st succ O in succ (succ A) holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ (succ A) & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) by Def11;
A3: ( succ A in succ (succ A) & A in succ A ) by ORDINAL1:6;
S . (succ A) = [{(S . A)},{}] by ORDINAL1:6, A2;
hence No_Ordinal_op (succ A) = [{(No_Ordinal_op A)},{}] by A3, A1, A2, Th63, ORDINAL1:10; :: thesis: verum