let C, A 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:62; :: thesis: verum