deffunc H₁( Ordinal, Ordinal) -> set = exp (a,$2);
deffunc H₂( Ordinal, Ordinal-Sequence) -> set = lim $2;
( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ b & fi . 0 = 1 & ( for c being Ordinal st succ c in succ b holds
fi . (succ c) = H₁(c,fi . c) ) & ( for c being Ordinal st c in succ b & 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 b & fi . 0 = 1 & ( for C being Ordinal st succ C in succ b holds
fi . (succ C) = H₁(C,fi . C) ) & ( for C being Ordinal st C in succ b & 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 b & fi . 0 = 1 & ( for C being Ordinal st succ C in succ b holds
fi . (succ C) = H₁(C,fi . C) ) & ( for C being Ordinal st C in succ b & 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 b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & 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 b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ex phi being Ordinal-Sequence st
( b₂ = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b₁ = b₂ ) ) ; :: thesis: verum