let A, C be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) holds
exp C,A is_limes_of fi )
assume that
A1: A <> {} and
A2: A is limit_ordinal ; :: thesis: for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) holds
exp C,A is_limes_of fi
consider psi being Ordinal-Sequence such that
A3: dom psi = A and
A4: for B being Ordinal st B in A holds
psi . B = exp C,B and
A5: ex D being Ordinal st D is_limes_of psi by A1, A2, Lm8;
let fi be Ordinal-Sequence; :: thesis: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) implies exp C,A is_limes_of fi )
assume that
A6: dom fi = A and
A7: for B being Ordinal st B in A holds
fi . B = exp C,B ; :: thesis: exp C,A is_limes_of fi

now

let x be set ; :: thesis: ( x in A implies fi . x = psi . x )
assume A8: x in A ; :: thesis: fi . x = psi . x
then reconsider B = x as Ordinal ;
thus fi . x = exp C,B by A7, A8
.= psi . x by A4, A8 ; :: thesis: verum

end;

then fi = psi by A6, A3, FUNCT_1:9;
then consider D being Ordinal such that
A9: D is_limes_of fi by A5;
D = lim fi by A9, ORDINAL2:def 14
.= exp C,A by A1, A2, A6, A7, ORDINAL2:62 ;
hence exp C,A is_limes_of fi by A9; :: thesis: verum