scheme :: POLNOT_1:sch 1
AInd{ F1() -> FinSequence-membered set , F2() -> Function of F1(),NAT, P1[ object ] } :
for a being object st a in Polish-expression-set (F1(),F2()) holds
P1[a]
provided
A1: for p, q being FinSequence
for n being Nat st p in F1() & n = F2() . p & q in (Polish-expression-set (F1(),F2())) ^^ n holds
P1[p ^ q]