deffunc H₁( Ordinal) -> set = C +^ (fi . $1);
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