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