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)) ^^ 1 & G in (Polish-WFF-set (L,E)) ^^ 1 ) ;
then F ^ G in (Polish-WFF-set (L,E)) ^^ (1 + 1) by Th11;
then reconsider u = F ^ G as Element of (Polish-WFF-set (L,E)) ^^ (E . t) by A1;
(Polish-binOp (L,E,t)) . (F,G) = (Polish-operation (L,E,t)) . u by A1, Def28;
hence ( Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t & Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> ) by A1, Th64; :: thesis: verum