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