let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for t being Element of L st E . t = 2 holds
for F being Polish-WFF of L,E st Polish-WFF-head F = t holds
ex G, H being Polish-WFF of L,E st F = (Polish-binOp (L,E,t)) . (G,H)
let E be Polish-arity-function of L; :: thesis: for t being Element of L st E . t = 2 holds
for F being Polish-WFF of L,E st Polish-WFF-head F = t holds
ex G, H being Polish-WFF of L,E st F = (Polish-binOp (L,E,t)) . (G,H)
let t be Element of L; :: thesis: ( E . t = 2 implies for F being Polish-WFF of L,E st Polish-WFF-head F = t holds
ex G, H being Polish-WFF of L,E st F = (Polish-binOp (L,E,t)) . (G,H) )
assume A1: E . t = 2 ; :: thesis: for F being Polish-WFF of L,E st Polish-WFF-head F = t holds
ex G, H being Polish-WFF of L,E st F = (Polish-binOp (L,E,t)) . (G,H)
let F be Polish-WFF of L,E; :: thesis: ( Polish-WFF-head F = t implies ex G, H being Polish-WFF of L,E st F = (Polish-binOp (L,E,t)) . (G,H) )
assume A2: Polish-WFF-head F = t ; :: thesis: ex G, H being Polish-WFF of L,E st F = (Polish-binOp (L,E,t)) . (G,H)
set W = Polish-WFF-set (L,E);
consider u being Element of (Polish-WFF-set (L,E)) ^^ 2 such that
A3: F = (Polish-operation (L,E,t)) . u by A1, A2, Th79;
(Polish-WFF-set (L,E)) ^^ 2 = (Polish-WFF-set (L,E)) ^^ (1 + 1)
.= ((Polish-WFF-set (L,E)) ^^ 1) ^ (Polish-WFF-set (L,E)) by Th6
.= (Polish-WFF-set (L,E)) ^ (Polish-WFF-set (L,E)) ;
then consider G, H being FinSequence such that
A5: u = G ^ H and
A6: G in Polish-WFF-set (L,E) and
A7: H in Polish-WFF-set (L,E) by Def2;
reconsider G = G as Element of Polish-WFF-set (L,E) by A6;
reconsider H = H as Element of Polish-WFF-set (L,E) by A7;
take G ; :: thesis: ex H being Polish-WFF of L,E st F = (Polish-binOp (L,E,t)) . (G,H)
take H ; :: thesis: F = (Polish-binOp (L,E,t)) . (G,H)
thus F = (Polish-binOp (L,E,t)) . (G,H) by A1, A3, A5, Def28; :: thesis: verum