let A be Ordinal; ( 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
; 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; ( 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)
; 0 is_limes_of fi
per cases
( 0 = 0 or 0 <> 0 )
;
ORDINAL2:def 9case
0 = 0
;
ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = 0 ) ) )take B = 1;
( B in dom fi & ( for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = 0 ) ) )
{} in A
by A1, ORDINAL3:8;
hence
B in dom fi
by A2, A3, Lm3, ORDINAL1:28;
for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = 0 )let D be
Ordinal;
( 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
;
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;
verum end; case
0 <> 0
;
for b1, b2 being set holds
( not b1 in 0 or not 0 in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )thus
for
b1,
b2 being
set holds
( not
b1 in 0 or not
0 in b2 or ex
b3 being
set st
(
b3 in dom fi & ( for
b4 being
set holds
( not
b3 c= b4 or not
b4 in dom fi or (
b1 in fi . b4 &
fi . b4 in b2 ) ) ) ) )
;
verum end; end;