let UN be non trivial Universe; :: thesis: for X being non empty set st X in UN holds
X * in UN
let X be non empty set ; :: thesis: ( X in UN implies X * in UN )
assume A1: X in UN ; :: thesis: X * in UN
consider f being Function such that
A2: dom f = NAT and
A3: for n being Nat holds f . n = n -tuples_on X and
A4: union (rng f) = X * by Th63;

now :: thesis: ( UN is FamUnion-closed & dom f = omega & rng f c= UN )

thus UN is FamUnion-closed ; :: thesis: ( dom f = omega & rng f c= UN )
thus dom f = omega by A2; :: thesis: rng f c= UN

now :: thesis: for x being object st x in rng f holds
x in UN

let x be object ; :: thesis: ( x in rng f implies x in UN )
assume x in rng f ; :: thesis: x in UN
then consider y being object such that
A5: y in dom f and
A6: x = f . y by FUNCT_1:def 3;
reconsider y = y as Nat by A5, A2;
y -tuples_on X in UN by A1, Th58;
hence x in UN by A6, A3; :: thesis: verum

end;

hence rng f c= UN ; :: thesis: verum

end;

hence X * in UN by Def6, A4; :: thesis: verum