let A, C be Ordinal; :: thesis: ( 1 in C & 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) = sup fi )
assume that
A1: 1 in C and
A2: A <> {} and
A3: 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) = sup 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) = sup fi )
assume that
A4: dom fi = A and
A5: for B being Ordinal st B in A holds
fi . B = exp (C,B) ; :: thesis: exp (C,A) = sup fi
fi is increasing by A1, A4, A5, Th25;
then lim fi = sup fi by A2, A3, A4, Th8;
hence exp (C,A) = sup fi by A2, A3, A4, A5, ORDINAL2:45; :: thesis: verum