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 st Polish-WFF-head F = t holds
ex G being Polish-WFF of L,E st F = (Polish-unOp (L,E,t)) . G
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 st Polish-WFF-head F = t holds
ex G being Polish-WFF of L,E st F = (Polish-unOp (L,E,t)) . G
let t be Element of L; :: thesis: ( E . t = 1 implies for F being Polish-WFF of L,E st Polish-WFF-head F = t holds
ex G being Polish-WFF of L,E st F = (Polish-unOp (L,E,t)) . G )
assume A1: E . t = 1 ; :: thesis: for F being Polish-WFF of L,E st Polish-WFF-head F = t holds
ex G being Polish-WFF of L,E st F = (Polish-unOp (L,E,t)) . G
let F be Polish-WFF of L,E; :: thesis: ( Polish-WFF-head F = t implies ex G being Polish-WFF of L,E st F = (Polish-unOp (L,E,t)) . G )
assume A2: Polish-WFF-head F = t ; :: thesis: ex G being Polish-WFF of L,E st F = (Polish-unOp (L,E,t)) . G
consider u being Element of (Polish-WFF-set (L,E)) ^^ 1 such that
A3: F = (Polish-operation (L,E,t)) . u by A1, A2, Th79;
reconsider G = u as Polish-WFF of L,E ;
take G ; :: thesis: F = (Polish-unOp (L,E,t)) . G
thus F = (Polish-unOp (L,E,t)) . G by A1, A3, Def27; :: thesis: verum