let A be Ordinal; :: thesis: ( A <> {} implies for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds

fi . B = exp (1,B) ) holds

1 is_limes_of fi )

assume A1: A <> {} ; :: thesis: for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds

fi . B = exp (1,B) ) holds

1 is_limes_of fi

let fi be Ordinal-Sequence; :: thesis: ( dom fi = A & ( for B being Ordinal st B in A holds

fi . B = exp (1,B) ) implies 1 is_limes_of fi )

assume that

A2: dom fi = A and

A3: for B being Ordinal st B in A holds

fi . B = exp (1,B) ; :: thesis: 1 is_limes_of fi

fi . B = exp (1,B) ) holds

1 is_limes_of fi )

assume A1: A <> {} ; :: thesis: for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds

fi . B = exp (1,B) ) holds

1 is_limes_of fi

let fi be Ordinal-Sequence; :: thesis: ( dom fi = A & ( for B being Ordinal st B in A holds

fi . B = exp (1,B) ) implies 1 is_limes_of fi )

assume that

A2: dom fi = A and

A3: for B being Ordinal st B in A holds

fi . B = exp (1,B) ; :: thesis: 1 is_limes_of fi

per cases
( 1 = 0 or 1 <> 0 )
;

:: according to ORDINAL2:def 9end;

:: according to ORDINAL2:def 9

case
1 = 0
; :: thesis: ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or fi . b_{2} = 0 ) ) )

( b

( not b

hence
ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or fi . b_{2} = 0 ) ) )
; :: thesis: verum

end;( b

( not b

case
1 <> 0
; :: thesis: for b_{1}, b_{2} being set holds

( not b_{1} in 1 or not 1 in b_{2} or ex b_{3} being set st

( b_{3} in dom fi & ( for b_{4} being set holds

( not b_{3} c= b_{4} or not b_{4} in dom fi or ( b_{1} in fi . b_{4} & fi . b_{4} in b_{2} ) ) ) ) )

( not b

( b

( not b

let A1, A2 be Ordinal; :: thesis: ( not A1 in 1 or not 1 in A2 or ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or ( A1 in fi . b_{2} & fi . b_{2} in A2 ) ) ) ) )

assume that

A4: A1 in 1 and

A5: 1 in A2 ; :: thesis: ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or ( A1 in fi . b_{2} & fi . b_{2} in A2 ) ) ) )

take B = {} ; :: thesis: ( B in dom fi & ( for b_{1} being set holds

( not B c= b_{1} or not b_{1} in dom fi or ( A1 in fi . b_{1} & fi . b_{1} in A2 ) ) ) )

thus B in dom fi by A1, A2, ORDINAL3:8; :: thesis: for b_{1} being set holds

( not B c= b_{1} or not b_{1} in dom fi or ( A1 in fi . b_{1} & fi . b_{1} in A2 ) )

let D be Ordinal; :: thesis: ( not B c= D or not D in dom fi or ( A1 in fi . D & fi . D in A2 ) )

assume that

B c= D and

A6: D in dom fi ; :: thesis: ( A1 in fi . D & fi . D in A2 )

exp (1,D) = fi . D by A2, A3, A6;

hence ( A1 in fi . D & fi . D in A2 ) by A4, A5, ORDINAL2:46; :: thesis: verum

end;( b

( not b

assume that

A4: A1 in 1 and

A5: 1 in A2 ; :: thesis: ex b

( b

( not b

take B = {} ; :: thesis: ( B in dom fi & ( for b

( not B c= b

thus B in dom fi by A1, A2, ORDINAL3:8; :: thesis: for b

( not B c= b

let D be Ordinal; :: thesis: ( not B c= D or not D in dom fi or ( A1 in fi . D & fi . D in A2 ) )

assume that

B c= D and

A6: D in dom fi ; :: thesis: ( A1 in fi . D & fi . D in A2 )

exp (1,D) = fi . D by A2, A3, A6;

hence ( A1 in fi . D & fi . D in A2 ) by A4, A5, ORDINAL2:46; :: thesis: verum