let T be Polish-language; :: thesis: for A being Polish-arity-function of T
for F being Polish-WFF of T,A st T -head F in Polish-atoms (T,A) holds
F = T -head F
let A be Polish-arity-function of T; :: thesis: for F being Polish-WFF of T,A st T -head F in Polish-atoms (T,A) holds
F = T -head F
let F be Polish-WFF of T,A; :: thesis: ( T -head F in Polish-atoms (T,A) implies F = T -head F )
assume T -head F in Polish-atoms (T,A) ; :: thesis: F = T -head F
then Polish-arity F = 0 by Def7;
then T -tail F in (Polish-WFF-set (T,A)) ^^ 0 by Th67;
then T -tail F in {{}} by Th6;
then T -tail F = {} by TARSKI:def 1;
then F = (T -head F) ^ {} ;
hence F = T -head F by FINSEQ_1:34; :: thesis: verum