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

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