deffunc H₁( Ordinal, Ordinal) -> Ordinal = $2 |^|^ omega;
deffunc H₂( Ordinal, Ordinal-Sequence) -> set = lim $2;
( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ a & fi . 0 = omega |^|^ omega & ( for c being Ordinal st succ c in succ a holds
fi . (succ c) = H₁(c,fi . c) ) & ( for c being Ordinal st c in succ a & c <> 0 & c is limit_ordinal holds
fi . c = H₂(c,fi | c) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ a & fi . 0 = omega |^|^ omega & ( for C being Ordinal st succ C in succ a holds
fi . (succ C) = H₁(C,fi . C) ) & ( for C being Ordinal st C in succ a & C <> 0 & C is limit_ordinal holds
fi . C = H₂(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ a & fi . 0 = omega |^|^ omega & ( for C being Ordinal st succ C in succ a holds
fi . (succ C) = H₁(C,fi . C) ) & ( for C being Ordinal st C in succ a & C <> 0 & C is limit_ordinal holds
fi . C = H₂(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch 13();
hence ( ex b₁ being Ordinal ex phi being Ordinal-Sequence st
( b₁ = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ( for b₁, b₂ being Ordinal st ex phi being Ordinal-Sequence st
( b₁ = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ex phi being Ordinal-Sequence st
( b₂ = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b₁ = b₂ ) ) ; :: thesis: verum