let L be non trivial Polish-language; 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; 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; 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; ( 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 )
( 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
;
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
;
F = (Polish-operation (L,E,t)) . u
thus F =
t ^ u
by A3, Def10
.=
(Polish-operation (L,E,t)) . u
by A2, Def13
;
verum
end;
given u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) such that A20:
F = (Polish-operation (L,E,t)) . u
; Polish-WFF-head F = t
reconsider u = u as FinSequence ;
F = t ^ u
by A2, A20, Def13;
hence
Polish-WFF-head F = t
by Th17; verum