let K be non trivial Polish-language; :: thesis: for E being Polish-arity-function of K
for e being Element of K
for M being Extension of (Polish-WFF-set (K,E))
for F being Formula of M st E . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (K,M,e)) . G
let E be Polish-arity-function of K; :: thesis: for e being Element of K
for M being Extension of (Polish-WFF-set (K,E))
for F being Formula of M st E . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (K,M,e)) . G
let e be Element of K; :: thesis: for M being Extension of (Polish-WFF-set (K,E))
for F being Formula of M st E . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (K,M,e)) . G
let M be Extension of (Polish-WFF-set (K,E)); :: thesis: for F being Formula of M st E . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (K,M,e)) . G
let F be Formula of M; :: thesis: ( E . e = 1 & Polish-ext-head F = e implies ex G being Formula of M st F = (Polish-unOp (K,M,e)) . G )
assume that
A1: E . e = 1 and
A2: Polish-ext-head F = e ; :: thesis: ex G being Formula of M st F = (Polish-unOp (K,M,e)) . G
set G = K -tail F;
A5: M is (E) ;
A6: ( F is K -headed & K -head F = e ) by A2, Th10;
then K -tail F in M ^^ (E . e) by A5;
then reconsider G = K -tail F as Element of M by A1;
take G ; :: thesis: F = (Polish-unOp (K,M,e)) . G
thus F = e ^ G by A6
.= (Polish-unOp (K,M,e)) . G by A1, Def15r ; :: thesis: verum
thus verum ; :: thesis: verum