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 A1: ( A <> {} & 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
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 A2: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) ) ; :: thesis: exp C,A is_limes_of fi
consider psi being Ordinal-Sequence such that
A3: ( dom psi = A & ( for B being Ordinal st B in A holds
psi . B = exp C,B ) ) and
A4: ex D being Ordinal st D is_limes_of psi by A1, Lm8;

now

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

end;

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