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 G being Formula of M st E . e = 1 holds
Polish-ext-head ((Polish-unOp (K,M,e)) . G) = e
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 G being Formula of M st E . e = 1 holds
Polish-ext-head ((Polish-unOp (K,M,e)) . G) = e
let e be Element of K; :: thesis: for M being Extension of (Polish-WFF-set (K,E))
for G being Formula of M st E . e = 1 holds
Polish-ext-head ((Polish-unOp (K,M,e)) . G) = e
let M be Extension of (Polish-WFF-set (K,E)); :: thesis: for G being Formula of M st E . e = 1 holds
Polish-ext-head ((Polish-unOp (K,M,e)) . G) = e
let G be Formula of M; :: thesis: ( E . e = 1 implies Polish-ext-head ((Polish-unOp (K,M,e)) . G) = e )
set F = (Polish-unOp (K,M,e)) . G;
assume E . e = 1 ; :: thesis: Polish-ext-head ((Polish-unOp (K,M,e)) . G) = e
then (Polish-unOp (K,M,e)) . G = e ^ G by Def15r;
then ( (Polish-unOp (K,M,e)) . G is K -headed & K -head ((Polish-unOp (K,M,e)) . G) = e ) ;
hence Polish-ext-head ((Polish-unOp (K,M,e)) . G) = e by Th32; :: thesis: verum