set X = { (P ^^ n) where n is Nat : verum } ;
set U = union { (P ^^ n) where n is Nat : verum } ;
for a being object st a in union { (P ^^ n) where n is Nat : verum } holds
a is FinSequence

proof

let a be object ; :: thesis: ( a in union { (P ^^ n) where n is Nat : verum } implies a is FinSequence )
assume a in union { (P ^^ n) where n is Nat : verum } ; :: thesis: a is FinSequence
then consider Y being set such that
A3: a in Y and
A4: Y in { (P ^^ n) where n is Nat : verum } by TARSKI:def 4;
consider n being Nat such that
A5: Y = P ^^ n by A4;
thus a is FinSequence by A3, A5; :: thesis: verum

end;

then A1: union { (P ^^ n) where n is Nat : verum } is FinSequence-membered ;
( {} in P ^^ 0 & P ^^ 0 in { (P ^^ n) where n is Nat : verum } ) by Th4;
hence union { (P ^^ n) where n is Nat : verum } is non empty FinSequence-membered set by A1, TARSKI:def 4; :: thesis: verum