let a be ordinal number ; :: thesis: for U being Universe st a in U holds
for f being Ordinal-Sequence of a,U holds Union f in U
let U be Universe; :: thesis: ( a in U implies for f being Ordinal-Sequence of a,U holds Union f in U )
assume Z0: a in U ; :: thesis: for f being Ordinal-Sequence of a,U holds Union f in U
let f be Ordinal-Sequence of a,U; :: thesis: Union f in U
dom f = a by FUNCT_2:def 1;
then ( card (dom f) in card U & card (rng f) c= card (dom f) & rng f c= On U & On U c= U ) by Z0, CARD_2:61, CLASSES2:1, ORDINAL2:7, RELAT_1:def 19;
then ( card (rng f) in card U & rng f c= U ) by ORDINAL1:12, XBOOLE_1:1;
then rng f in U by CLASSES1:1;
hence Union f in U by CLASSES2:59; :: thesis: verum