let fi be Ordinal-Sequence; :: thesis: for A, B being Ordinal st A is_limes_of fi holds
B +^ A is_limes_of B +^ fi
let A, B be Ordinal; :: thesis: ( A is_limes_of fi implies B +^ A is_limes_of B +^ fi )
assume A1: ( ( A = {} & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) or ( A <> {} & ( for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def 13 :: thesis: B +^ A is_limes_of B +^ fi
A2: dom fi = dom (B +^ fi) by ORDINAL3:def 2;

per cases ( B +^ A = {} or B +^ A <> {} ) ;
:: according to ORDINAL2:def 13

case A3: B +^ A = {} ; :: thesis: ex b₁ being set st
( b₁ in dom (B +^ fi) & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom (B +^ fi) or (B +^ fi) . b₂ = {} ) ) )

then consider A1 being Ordinal such that
A4: ( A1 in dom fi & ( for C being Ordinal st A1 c= C & C in dom fi holds
fi . C = {} ) ) by A1, ORDINAL3:29;
take A1 ; :: thesis: ( A1 in dom (B +^ fi) & ( for b₁ being set holds
( not A1 c= b₁ or not b₁ in dom (B +^ fi) or (B +^ fi) . b₁ = {} ) ) )
thus A1 in dom (B +^ fi) by A4, ORDINAL3:def 2; :: thesis: for b₁ being set holds
( not A1 c= b₁ or not b₁ in dom (B +^ fi) or (B +^ fi) . b₁ = {} )
let C be Ordinal; :: thesis: ( not A1 c= C or not C in dom (B +^ fi) or (B +^ fi) . C = {} )
assume ( A1 c= C & C in dom (B +^ fi) ) ; :: thesis: (B +^ fi) . C = {}
then ( (B +^ fi) . C = B +^ (fi . C) & fi . C = {} & {} = {} ) by A2, A4, ORDINAL3:def 2;
hence (B +^ fi) . C = {} by A3, ORDINAL3:29; :: thesis: verum

end;

case B +^ A <> {} ; :: thesis: for b₁, b₂ being set holds
( not b₁ in B +^ A or not B +^ A in b₂ or ex b₃ being set st
( b₃ in dom (B +^ fi) & ( for b₄ being set holds
( not b₃ c= b₄ or not b₄ in dom (B +^ fi) or ( b₁ in (B +^ fi) . b₄ & (B +^ fi) . b₄ in b₂ ) ) ) ) )

now

per cases ( A = {} or A <> {} ) ;

suppose A5: A = {} ; :: thesis: for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds
ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

then consider A1 being Ordinal such that
A6: ( A1 in dom fi & ( for C being Ordinal st A1 c= C & C in dom fi holds
fi . C = {} ) ) by A1;
let B1, B2 be Ordinal; :: thesis: ( B1 in B +^ A & B +^ A in B2 implies ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )
assume A7: ( B1 in B +^ A & B +^ A in B2 ) ; :: thesis: ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
take A1 = A1; :: thesis: ( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
thus A1 in dom (B +^ fi) by A6, ORDINAL3:def 2; :: thesis: for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )
let C be Ordinal; :: thesis: ( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )
assume ( A1 c= C & C in dom (B +^ fi) ) ; :: thesis: ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )
then ( (B +^ fi) . C = B +^ (fi . C) & fi . C = {} & {} = {} ) by A2, A6, ORDINAL3:def 2;
hence ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) by A5, A7; :: thesis: verum

end;

suppose A8: A <> {} ; :: thesis: for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds
ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

let B1, B2 be Ordinal; :: thesis: ( B1 in B +^ A & B +^ A in B2 implies ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )
assume ( B1 in B +^ A & B +^ A in B2 ) ; :: thesis: ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
then A9: ( B1 -^ B in A & A in B2 -^ B & B +^ A c= B2 ) by A8, ORDINAL1:def 2, ORDINAL3:73, ORDINAL3:74;
then consider A1 being Ordinal such that
A10: ( A1 in dom fi & ( for C being Ordinal st A1 c= C & C in dom fi holds
( B1 -^ B in fi . C & fi . C in B2 -^ B ) ) ) by A1;
take A1 = A1; :: thesis: ( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
thus A1 in dom (B +^ fi) by A10, ORDINAL3:def 2; :: thesis: for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )
B c= B +^ A by ORDINAL3:27;
then A11: ( B c= B2 & B1 c= B +^ (B1 -^ B) ) by A9, ORDINAL3:75, XBOOLE_1:1;
let C be Ordinal; :: thesis: ( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )
assume A12: ( A1 c= C & C in dom (B +^ fi) ) ; :: thesis: ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )
reconsider E = fi . C as Ordinal ;
A13: ( (B +^ fi) . C = B +^ (fi . C) & B1 -^ B in E & E in B2 -^ B & E = E & B +^ (B2 -^ B) = B2 ) by A2, A10, A11, A12, ORDINAL3:def 2, ORDINAL3:def 6;
then B +^ (B1 -^ B) in B +^ E by ORDINAL2:49;
hence ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) by A11, A13, ORDINAL1:22, ORDINAL2:49; :: thesis: verum

end;

end;

end;

hence for A1, C being Ordinal st A1 in B +^ A & B +^ A in C holds
ex D being Ordinal st
( D in dom (B +^ fi) & ( for E being Ordinal st D c= E & E in dom (B +^ fi) holds
( A1 in (B +^ fi) . E & (B +^ fi) . E in C ) ) ) ; :: thesis: verum

end;

end;