let P be FinSequence-membered set ; :: thesis: for a being object holds
( a in P * iff ex n being Nat st a in P ^^ n )
let a be object ; :: thesis: ( a in P * iff ex n being Nat st a in P ^^ n )
set X = { (P ^^ n) where n is Nat : verum } ;
thus ( a in P * implies ex n being Nat st a in P ^^ n ) :: thesis: ( ex n being Nat st a in P ^^ n implies a in P * )

proof

assume a in P * ; :: thesis: ex n being Nat st a in P ^^ n
then consider Y being set such that
A1: a in Y and
A2: Y in { (P ^^ n) where n is Nat : verum } by TARSKI:def 4;
consider n being Nat such that
A3: Y = P ^^ n by A2;
take n ; :: thesis: a in P ^^ n
thus a in P ^^ n by A1, A3; :: thesis: verum

end;

given n being Nat such that A4: a in P ^^ n ; :: thesis: a in P *
P ^^ n in { (P ^^ n) where n is Nat : verum } ;
hence a in P * by A4, TARSKI:def 4; :: thesis: verum