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
per cases ( 1 = 0 or 1 <> 0 ) ;
:: according to ORDINAL2:def 9
case 1 = 0 ; :: 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 = 0 ) ) )
hence 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 ) ) ) ; :: thesis: verum
end;
case 1 <> 0 ; :: thesis: for b1, b2 being set holds
( not b1 in 1 or not 1 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 ) ) ) ) )
let A1, A2 be Ordinal; :: thesis: ( not A1 in 1 or not 1 in A2 or 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 ( A1 in fi . b2 & fi . b2 in A2 ) ) ) ) )
assume that
A4: A1 in 1 and
A5: 1 in A2 ; :: 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 ( A1 in fi . b2 & fi . b2 in A2 ) ) ) )
take B = {} ; :: thesis: ( B in dom fi & ( for b1 being set holds
( not B c= b1 or not b1 in dom fi or ( A1 in fi . b1 & fi . b1 in A2 ) ) ) )
thus B in dom fi by A1, A2, ORDINAL3:8; :: thesis: for b1 being set holds
( not B c= b1 or not b1 in dom fi or ( A1 in fi . b1 & fi . b1 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;
end;