deffunc H1( set , Sequence) -> set = union (rng $2);
deffunc H2( Ordinal, set ) -> set = new_set2 $2;
let A be non empty set ; for O being Ordinal
for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveSet2 (A,O1) ) holds
ConsecutiveSet2 (A,O) = union (rng T)
let O be Ordinal; for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveSet2 (A,O1) ) holds
ConsecutiveSet2 (A,O) = union (rng T)
let T be Sequence; ( O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveSet2 (A,O1) ) implies ConsecutiveSet2 (A,O) = union (rng T) )
deffunc H3( Ordinal) -> set = ConsecutiveSet2 (A,$1);
assume that
A1:
( O <> 0 & O is limit_ordinal )
and
A2:
dom T = O
and
A3:
for O1 being Ordinal st O1 in O holds
T . O1 = H3(O1)
; ConsecutiveSet2 (A,O) = union (rng T)
A4:
for O being Ordinal
for It being object holds
( It = H3(O) iff ex L0 being Sequence st
( It = last L0 & dom L0 = succ O & L0 . 0 = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H2(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = H1(C,L0 | C) ) ) )
by Def5;
thus
H3(O) = H1(O,T)
from ORDINAL2:sch 10(A4, A1, A2, A3); verum