let B be Polish-arity-function; :: thesis: for C being Extension of B
for e being Element of dom C
for M being Polish-ext-set of C
for G being Formula of M st C . e = 1 holds
Polish-ext-head ((Polish-unOp (C,M,e)) . G) = e
let C be Extension of B; :: thesis: for e being Element of dom C
for M being Polish-ext-set of C
for G being Formula of M st C . e = 1 holds
Polish-ext-head ((Polish-unOp (C,M,e)) . G) = e
let e be Element of dom C; :: thesis: for M being Polish-ext-set of C
for G being Formula of M st C . e = 1 holds
Polish-ext-head ((Polish-unOp (C,M,e)) . G) = e
let M be Polish-ext-set of C; :: thesis: for G being Formula of M st C . e = 1 holds
Polish-ext-head ((Polish-unOp (C,M,e)) . G) = e
let G be Formula of M; :: thesis: ( C . e = 1 implies Polish-ext-head ((Polish-unOp (C,M,e)) . G) = e )
set K = dom C;
set F = (Polish-unOp (C,M,e)) . G;
assume C . e = 1 ; :: thesis: Polish-ext-head ((Polish-unOp (C,M,e)) . G) = e
then (Polish-unOp (C,M,e)) . G = e ^ G by Def15;
then ( (Polish-unOp (C,M,e)) . G is dom C -headed & (dom C) -head ((Polish-unOp (C,M,e)) . G) = e ) ;
hence Polish-ext-head ((Polish-unOp (C,M,e)) . G) = e by Th12; :: thesis: verum