set S = Polish-WFF-set (T,A);
let s be FinSequence; :: according to POLNOT_2:def 10 :: thesis: ( s in Polish-WFF-set (T,A) & s is T -headed implies T -tail s in (Polish-WFF-set (T,A)) ^^ (A . (T -head s)) )
assume s in Polish-WFF-set (T,A) ; :: thesis: ( not s is T -headed or T -tail s in (Polish-WFF-set (T,A)) ^^ (A . (T -head s)) )
then reconsider F = s as Polish-WFF of T,A ;
A . (T -head s) = A . (Polish-WFF-head F) by POLNOT_1:def 33
.= Polish-arity F by POLNOT_1:def 35 ;
hence ( not s is T -headed or T -tail s in (Polish-WFF-set (T,A)) ^^ (A . (T -head s)) ) by POLNOT_1:67; :: thesis: verum