set V = Polish-expression-set (F₁(),F₂());
consider U being set such that
A2: for a being object holds
( a in U iff ( a in Polish-expression-set (F₁(),F₂()) & P₁[a] ) ) from XBOOLE_0:sch 1();
A3: U c= Polish-expression-set (F₁(),F₂()) by A2;
then reconsider U = U as Subset of (F₁() *) by XBOOLE_1:1;
U is F₂() -closed

proof

let p be FinSequence; :: according to POLNOT_1:def 15 :: thesis: for n being Nat
for q being FinSequence st p in dom F₂() & n = F₂() . p & q in U ^^ n holds
p ^ q in U
let n be Nat; :: thesis: for q being FinSequence st p in dom F₂() & n = F₂() . p & q in U ^^ n holds
p ^ q in U
let q be FinSequence; :: thesis: ( p in dom F₂() & n = F₂() . p & q in U ^^ n implies p ^ q in U )
assume that
A4: p in dom F₂() and
A5: n = F₂() . p and
A6: q in U ^^ n ; :: thesis: p ^ q in U
A7: dom F₂() = F₁() by FUNCT_2:def 1;
A8: U ^^ n c= (Polish-expression-set (F₁(),F₂())) ^^ n by A3, Th17;
then A9: P₁[p ^ q] by A1, A4, A5, A6, A7;
Polish-expression-set (F₁(),F₂()) is F₂() -closed ;
hence p ^ q in U by A2, A4, A5, A6, A8, A9; :: thesis: verum

end;

then Polish-expression-set (F₁(),F₂()) c= U by Th37;
hence for a being object st a in Polish-expression-set (F₁(),F₂()) holds
P₁[a] by A2; :: thesis: verum