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 A1: ( 1 in C & 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 = 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 A2: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) ) ; :: thesis: exp C,A = sup fi
then fi is increasing by A1, Th25;
then lim fi = sup fi by A1, A2, Th8;
hence exp C,A = sup fi by A1, A2, ORDINAL2:62; :: thesis: verum