let a be Ordinal; :: thesis: a |^|^ 0 = 1
deffunc H₁( Ordinal) -> Ordinal = a |^|^ $1;
deffunc H₂( Ordinal, Ordinal-Sequence) -> set = lim $2;
deffunc H₃( Ordinal, Ordinal) -> set = exp (a,$2);
A1: 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₁( 0 ) = 1 from ORDINAL2:sch 14(A1); :: thesis: verum