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 that
A1: dom phi = M and
A2: rng phi c= N and
A3: M in cf N ; :: thesis: ( sup phi in N & Union phi in N )
card (rng phi) c= card M by A1, CARD_1:12;
then card (rng phi) in cf N by A3, ORDINAL1:12;
hence ( sup phi in N & Union phi in N ) by A2, Th25; :: thesis: verum