deffunc H₁( Ordinal) -> Ordinal = inf (rng (L | ((dom L) \ $1)));
consider fi being Ordinal-Sequence such that
A7: ( dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = H₁(A) ) ) from ORDINAL2:sch 3();
take sup fi ; :: thesis: ex fi being Ordinal-Sequence st
( sup fi = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
take fi ; :: thesis: ( sup fi = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
thus ( sup fi = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) by A7; :: thesis: verum