let M, N be Cardinal; :: thesis: for phi being Ordinal-Sequence st dom phi = M & rng phi c= N & M in cf N holds
( sup phi in N & Union phi in N )
let phi be Ordinal-Sequence; :: thesis: ( dom phi = M & rng phi c= N & M in cf N implies ( sup phi in N & Union phi in N ) )
assume A1: ( dom phi = M & rng phi c= N & M in cf N ) ; :: thesis: ( sup phi in N & Union phi in N )
then ( card (rng phi) c= card M & card M = M ) by CARD_1:28, CARD_1:def 5;
then ( card (rng phi) in cf N & Union phi = union (rng phi) & sup phi = sup (rng phi) ) by A1, ORDINAL1:22;
hence ( sup phi in N & Union phi in N ) by A1, Th38; :: thesis: verum