let P be FinSequence-membered set ; :: thesis: {} in P ^^ 0
P ^^ 0 = {{}} by Def3;
hence {} in P ^^ 0 by TARSKI:def 1; :: thesis: verum