let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for t being Element of L
for F being Polish-WFF of L,E holds
( Polish-WFF-head F = t iff ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u )
let E be Polish-arity-function of L; :: thesis: for t being Element of L
for F being Polish-WFF of L,E holds
( Polish-WFF-head F = t iff ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u )
let t be Element of L; :: thesis: for F being Polish-WFF of L,E holds
( Polish-WFF-head F = t iff ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u )
let F be Polish-WFF of L,E; :: thesis: ( Polish-WFF-head F = t iff ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u )
set W = Polish-WFF-set (L,E);
set H = Polish-operation (L,E,t);
A2: dom (Polish-operation (L,E,t)) = (Polish-WFF-set (L,E)) ^^ (E . t) by FUNCT_2:def 1;
thus ( Polish-WFF-head F = t implies ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u ) :: thesis: ( ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u implies Polish-WFF-head F = t )

proof

assume A3: Polish-WFF-head F = t ; :: thesis: ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u
set u = (L,E) -tail F;
reconsider u = (L,E) -tail F as Element of (Polish-WFF-set (L,E)) ^^ (E . t) by A3;
take u ; :: thesis: F = (Polish-operation (L,E,t)) . u
thus F = t ^ u by A3
.= (Polish-operation (L,E,t)) . u by A2, Def12 ; :: thesis: verum

end;

given u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) such that A20: F = (Polish-operation (L,E,t)) . u ; :: thesis: Polish-WFF-head F = t
reconsider u = u as FinSequence ;
thus Polish-WFF-head F = t by A20; :: thesis: verum