deffunc H₁( Ordinal) -> set = (fi . $1) +^ C;
thus ex F being Ordinal-Sequence st
( dom F = dom fi & ( for A being Ordinal st A in dom fi holds
F . A = H₁(A) ) ) from ORDINAL2:sch 3(); :: thesis: verum