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 F being Formula of M st C . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (C,M,e)) . G
let C be Extension of B; :: thesis: for e being Element of dom C
for M being Polish-ext-set of C
for F being Formula of M st C . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (C,M,e)) . G
let e be Element of dom C; :: thesis: for M being Polish-ext-set of C
for F being Formula of M st C . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (C,M,e)) . G
let M be Polish-ext-set of C; :: thesis: for F being Formula of M st C . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (C,M,e)) . G
let F be Formula of M; :: thesis: ( C . e = 1 & Polish-ext-head F = e implies ex G being Formula of M st F = (Polish-unOp (C,M,e)) . G )
set K = dom C;
assume that
A1: C . e = 1 and
A2: Polish-ext-head F = e ; :: thesis: ex G being Formula of M st F = (Polish-unOp (C,M,e)) . G
set G = (dom C) -tail F;
A5: M is C -compatible ;
A6: ( F is dom C -headed & (dom C) -head F = e ) by A2, Th10;
then consider n being Nat such that
A8: ( n = C . e & (dom C) -tail F in M ^^ n ) by A5;
reconsider G = (dom C) -tail F as Element of M by A1, A8;
take G ; :: thesis: F = (Polish-unOp (C,M,e)) . G
thus F = e ^ G by A6
.= (Polish-unOp (C,M,e)) . G by A1, Def15 ; :: thesis: verum
thus verum ; :: thesis: verum