let B be Polish-arity-function; :: thesis: for C being Extension of B
for e being Element of dom C
for M being Polish-ext-set of C
for G, H being Formula of M st C . e = 2 holds
Polish-ext-head ((Polish-binOp (C,M,e)) . (G,H)) = e
let C be Extension of B; :: thesis: for e being Element of dom C
for M being Polish-ext-set of C
for G, H being Formula of M st C . e = 2 holds
Polish-ext-head ((Polish-binOp (C,M,e)) . (G,H)) = e
let e be Element of dom C; :: thesis: for M being Polish-ext-set of C
for G, H being Formula of M st C . e = 2 holds
Polish-ext-head ((Polish-binOp (C,M,e)) . (G,H)) = e
let M be Polish-ext-set of C; :: thesis: for G, H being Formula of M st C . e = 2 holds
Polish-ext-head ((Polish-binOp (C,M,e)) . (G,H)) = e
let G, H be Formula of M; :: thesis: ( C . e = 2 implies Polish-ext-head ((Polish-binOp (C,M,e)) . (G,H)) = e )
set F = (Polish-binOp (C,M,e)) . (G,H);
set K = dom C;
assume A1: C . e = 2 ; :: thesis: Polish-ext-head ((Polish-binOp (C,M,e)) . (G,H)) = e
(Polish-binOp (C,M,e)) . (G,H) = e ^ (G ^ H) by A1, Def16;
then ( (Polish-binOp (C,M,e)) . (G,H) is dom C -headed & (dom C) -head ((Polish-binOp (C,M,e)) . (G,H)) = e ) ;
hence Polish-ext-head ((Polish-binOp (C,M,e)) . (G,H)) = e by Th12; :: thesis: verum