consider S being Sequence such that
A1: ( No_Ordinal_op 0 = S . 0 & dom S = succ 0 ) and
A2: ( ( for O being Ordinal st succ O in succ 0 holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ 0 & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) by Def11;
S . 0 = [(rng (S | 0)),{}] by A2, ORDINAL1:6, ORDINAL2:4;
hence No_Ordinal_op 0 = 0_No by A1; :: thesis: verum