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 = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (C,M,e)) . (G,H)
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 = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (C,M,e)) . (G,H)
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 = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (C,M,e)) . (G,H)
let M be Polish-ext-set of C; :: thesis: for F being Formula of M st C . e = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (C,M,e)) . (G,H)
let F be Formula of M; :: thesis: ( C . e = 2 & Polish-ext-head F = e implies ex G, H being Formula of M st F = (Polish-binOp (C,M,e)) . (G,H) )
set K = dom C;
assume that
A1: C . e = 2 and
A2: Polish-ext-head F = e ; :: thesis: ex G, H being Formula of M st F = (Polish-binOp (C,M,e)) . (G,H)
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
A7: ( n = C . e & (dom C) -tail F in M ^^ n ) by A5;
reconsider g = (dom C) -tail F as Element of M ^^ (1 + 1) by A1, A7;
M ^^ (1 + 1) = (M ^^ 1) ^ M by POLNOT_1:6;
then consider p, q being FinSequence such that
A8: g = p ^ q and
A9: p in M and
A10: q in M by POLNOT_1:def 2;
reconsider G = p, H = q as Formula of M by A9, A10;
take G ; :: thesis: ex H being Formula of M st F = (Polish-binOp (C,M,e)) . (G,H)
take H ; :: thesis: F = (Polish-binOp (C,M,e)) . (G,H)
thus F = e ^ (p ^ q) by A6, A8
.= (Polish-binOp (C,M,e)) . (G,H) by A1, Def16 ; :: thesis: verum
thus verum ; :: thesis: verum