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 :: thesis: for x being object st x in A holds
fi . x = psi . x

let x be object ; :: 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:2;
then consider D being Ordinal such that
A9: D is_limes_of fi by A5;
D = lim fi by A9, ORDINAL2:def 10
.= exp (C,A) by A1, A2, A6, A7, ORDINAL2:45 ;
hence exp (C,A) is_limes_of fi by A9; :: thesis: verum