let A be Ordinal; :: thesis: for fi being Ordinal-Sequence st A in dom fi holds
fi . A is Ordinal
let fi be Ordinal-Sequence; :: thesis: ( A in dom fi implies fi . A is Ordinal )
assume A in dom fi ; :: thesis: fi . A is Ordinal
then A1: fi . A in rng fi by FUNCT_1:def 5;
consider B being Ordinal such that
A2: rng fi c= B by Def8;
thus fi . A is Ordinal by A1, A2; :: thesis: verum