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 G, H being Formula of M st E . e = 2 holds
Polish-ext-head ((Polish-binOp (K,M,e)) . (G,H)) = e
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 G, H being Formula of M st E . e = 2 holds
Polish-ext-head ((Polish-binOp (K,M,e)) . (G,H)) = e
let e be Element of K; :: thesis: for M being Extension of (Polish-WFF-set (K,E))
for G, H being Formula of M st E . e = 2 holds
Polish-ext-head ((Polish-binOp (K,M,e)) . (G,H)) = e
let M be Extension of (Polish-WFF-set (K,E)); :: thesis: for G, H being Formula of M st E . e = 2 holds
Polish-ext-head ((Polish-binOp (K,M,e)) . (G,H)) = e
let G, H be Formula of M; :: thesis: ( E . e = 2 implies Polish-ext-head ((Polish-binOp (K,M,e)) . (G,H)) = e )
set F = (Polish-binOp (K,M,e)) . (G,H);
assume A1: E . e = 2 ; :: thesis: Polish-ext-head ((Polish-binOp (K,M,e)) . (G,H)) = e
(Polish-binOp (K,M,e)) . (G,H) = e ^ (G ^ H) by A1, Def16r;
then ( (Polish-binOp (K,M,e)) . (G,H) is K -headed & K -head ((Polish-binOp (K,M,e)) . (G,H)) = e ) ;
hence Polish-ext-head ((Polish-binOp (K,M,e)) . (G,H)) = e by Th32; :: thesis: verum