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, G being Polish-WFF of L,E holds
( Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t & Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> )
let E be Polish-arity-function of L; :: thesis: for t being Element of L st E . t = 2 holds
for F, G being Polish-WFF of L,E holds
( Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t & Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> )
let t be Element of L; :: thesis: ( E . t = 2 implies for F, G being Polish-WFF of L,E holds
( Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t & Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> ) )
assume A1: E . t = 2 ; :: thesis: for F, G being Polish-WFF of L,E holds
( Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t & Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> )
let F, G be Polish-WFF of L,E; :: thesis: ( Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t & Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> )
set W = Polish-WFF-set (L,E);
set H = Polish-binOp (L,E,t);
set K = Polish-operation (L,E,t);
set v = (Polish-binOp (L,E,t)) . (F,G);
( F in Polish-WFF-set (L,E) & G in Polish-WFF-set (L,E) ) ;
then ( F in (Polish-WFF-set (L,E)) ^^ 1 & G in (Polish-WFF-set (L,E)) ^^ 1 ) by Th8;
then F ^ G in (Polish-WFF-set (L,E)) ^^ (1 + 1) by Th12;
then reconsider u = F ^ G as Element of (Polish-WFF-set (L,E)) ^^ (E . t) by A1;
A5: (Polish-binOp (L,E,t)) . (F,G) = (Polish-operation (L,E,t)) . u by A1, Def22;
hence Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t by Th91; :: thesis: Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*>
hence Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> by A1, A5, Th56, Th65; :: thesis: verum