let a be Ordinal; :: 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 A1: 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 A1, 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;
then rng f in U by CLASSES1:1;
hence Union f in U by CLASSES2:59; :: thesis: verum