let A be Ordinal; :: thesis: ( 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 ({},B) ) holds

0 is_limes_of fi )

assume that

A1: A <> {} and

A2: 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 ({},B) ) holds

0 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 ({},B) ) implies 0 is_limes_of fi )

assume that

A3: dom fi = A and

A4: for B being Ordinal st B in A holds

fi . B = exp ({},B) ; :: thesis: 0 is_limes_of fi

fi . B = exp ({},B) ) holds

0 is_limes_of fi )

assume that

A1: A <> {} and

A2: 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 ({},B) ) holds

0 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 ({},B) ) implies 0 is_limes_of fi )

assume that

A3: dom fi = A and

A4: for B being Ordinal st B in A holds

fi . B = exp ({},B) ; :: thesis: 0 is_limes_of fi

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

:: according to ORDINAL2:def 9end;

:: according to ORDINAL2:def 9

case
0 = 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

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

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

{} in A by A1, ORDINAL3:8;

hence B in dom fi by A2, A3, Lm3, ORDINAL1:28; :: thesis: for b_{1} being set holds

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

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

assume that

A5: B c= D and

A6: D in dom fi ; :: thesis: fi . D = 0

A7: D <> {} by A5, Lm3, ORDINAL1:21;

exp ({},D) = fi . D by A3, A4, A6;

hence fi . D = 0 by A7, Th20; :: thesis: verum

end;( not B c= b

{} in A by A1, ORDINAL3:8;

hence B in dom fi by A2, A3, Lm3, ORDINAL1:28; :: thesis: for b

( not B c= b

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

assume that

A5: B c= D and

A6: D in dom fi ; :: thesis: fi . D = 0

A7: D <> {} by A5, Lm3, ORDINAL1:21;

exp ({},D) = fi . D by A3, A4, A6;

hence fi . D = 0 by A7, Th20; :: thesis: verum

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

( not b_{1} in 0 or not 0 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

thus
for b_{1}, b_{2} being set holds

( not b_{1} in 0 or not 0 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} ) ) ) ) )
; :: thesis: verum

end;( not b

( b

( not b