let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for t being Element of L st E . t = 1 holds
for F being Polish-WFF of L,E holds
( Polish-WFF-head ((Polish-unOp (L,E,t)) . F) = t & Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*> )
let E be Polish-arity-function of L; :: thesis: for t being Element of L st E . t = 1 holds
for F being Polish-WFF of L,E holds
( Polish-WFF-head ((Polish-unOp (L,E,t)) . F) = t & Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*> )
let t be Element of L; :: thesis: ( E . t = 1 implies for F being Polish-WFF of L,E holds
( Polish-WFF-head ((Polish-unOp (L,E,t)) . F) = t & Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*> ) )
assume A1: E . t = 1 ; :: thesis: for F being Polish-WFF of L,E holds
( Polish-WFF-head ((Polish-unOp (L,E,t)) . F) = t & Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*> )
let F be Polish-WFF of L,E; :: thesis: ( Polish-WFF-head ((Polish-unOp (L,E,t)) . F) = t & Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*> )
set W = Polish-WFF-set (L,E);
set H = Polish-unOp (L,E,t);
set G = (Polish-unOp (L,E,t)) . F;
reconsider F1 = F as Element of (Polish-WFF-set (L,E)) ^^ (E . t) by A1;
ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st (Polish-unOp (L,E,t)) . F = (Polish-operation (L,E,t)) . u

proof

take u = F1; :: thesis: (Polish-unOp (L,E,t)) . F = (Polish-operation (L,E,t)) . u
thus (Polish-unOp (L,E,t)) . F = (Polish-operation (L,E,t)) . u by A1, Def27; :: thesis: verum

end;

hence Polish-WFF-head ((Polish-unOp (L,E,t)) . F) = t ; :: thesis: Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*>
(Polish-unOp (L,E,t)) . F = (Polish-operation (L,E,t)) . F1 by A1, Def27;
hence Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*> by A1, Th63; :: thesis: verum