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

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

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

then
fi = psi
by A6, A3, FUNCT_1:2;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;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

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