deffunc H1( Ordinal, Ordinal) -> Ordinal = $2 |^|^ omega;
deffunc H2( 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) = H1(c,fi . c) ) & ( for c being Ordinal st c in succ a & c <> 0 & c is limit_ordinal holds
fi . c = H2(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) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ a & C <> 0 & C is limit_ordinal holds
fi . C = H2(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) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ a & C <> 0 & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) holds
A1 = A2 ) )
from ORDINAL2:sch 13();
hence
( ex b1 being Ordinal ex phi being Ordinal-Sequence st
( b1 = 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 b1, b2 being Ordinal st ex phi being Ordinal-Sequence st
( b1 = 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
( b2 = 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
b1 = b2 ) )
; verum