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 3;
ex B being Ordinal st rng fi c= B by Def4;
hence fi . A is Ordinal by A1; :: thesis: verum