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 = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (K,M,e)) . (G,H)
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 = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (K,M,e)) . (G,H)
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 = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (K,M,e)) . (G,H)
let M be Extension of (Polish-WFF-set (K,E)); :: thesis: for F being Formula of M st E . e = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (K,M,e)) . (G,H)
let F be Formula of M; :: thesis: ( E . e = 2 & Polish-ext-head F = e implies ex G, H being Formula of M st F = (Polish-binOp (K,M,e)) . (G,H) )
assume that
A1: E . e = 2 and
A2: Polish-ext-head F = e ; :: thesis: ex G, H being Formula of M st F = (Polish-binOp (K,M,e)) . (G,H)
set g = K -tail F;
A5: M is (E) ;
A6: ( F is K -headed & K -head F = e ) by A2, Th10;
then reconsider g = K -tail F as Element of M ^^ (1 + 1) by A1, A5;
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 (K,M,e)) . (G,H)
take H ; :: thesis: F = (Polish-binOp (K,M,e)) . (G,H)
thus F = e ^ (p ^ q) by A6, A8
.= (Polish-binOp (K,M,e)) . (G,H) by A1, Def16r ; :: thesis: verum
thus verum ; :: thesis: verum