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
{} 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
{} 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 {} 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: {} is_limes_of fi
per cases
( {} = {} or {} <> {} )
;
:: according to ORDINAL2:def 13case
{} = {}
;
:: thesis: 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 = {} ) ) )take B = 1;
:: thesis: ( B in dom fi & ( for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = {} ) ) )
{} in A
by A1, ORDINAL3:10;
hence
B in dom fi
by A2, A3, Lm3, ORDINAL1:41;
:: thesis: for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = {} )let D be
Ordinal;
:: thesis: ( not B c= D or not D in dom fi or fi . D = {} )assume that A5:
B c= D
and A6:
D in dom fi
;
:: thesis: fi . D = {} A7:
D <> {}
by A5, Lm3, ORDINAL1:33;
exp {} ,
D = fi . D
by A3, A4, A6;
hence
fi . D = {}
by A7, Th20;
:: thesis: verum end;