let a, b be Ordinal; :: thesis: ( b <> 0 & b is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = b & ( for c being Ordinal st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi )
assume A1: ( b <> 0 & b is limit_ordinal ) ; :: thesis: for phi being Ordinal-Sequence st dom phi = b & ( for c being Ordinal st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi
deffunc H₁( Ordinal) -> Ordinal = a |^|^ $1;
deffunc H₂( Ordinal, Ordinal-Sequence) -> set = lim $2;
deffunc H₃( Ordinal, Ordinal) -> set = exp (a,$2);
let fi be Ordinal-Sequence; :: thesis: ( dom fi = b & ( for c being Ordinal st c in b holds
fi . c = a |^|^ c ) implies a |^|^ b = lim fi )
assume that
A2: dom fi = b and
A3: for c being Ordinal st c in b holds
fi . c = H₁(c) ; :: thesis: a |^|^ b = lim fi
A4: for b, c being Ordinal holds
( c = H₁(b) iff ex fi being Ordinal-Sequence st
( c = 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) ) ) ) by Def4;
thus H₁(b) = H₂(b,fi) from ORDINAL2:sch 16(A4, A1, A2, A3); :: thesis: verum