let B be Polish-arity-function; :: thesis: for J being Polish-ext-set of B
for F being Formula of J st F is dom B -headed holds
Polish-ext-head F = (dom B) -head F
let J be Polish-ext-set of B; :: thesis: for F being Formula of J st F is dom B -headed holds
Polish-ext-head F = (dom B) -head F
set T = dom B;
let F be Formula of J; :: thesis: ( F is dom B -headed implies Polish-ext-head F = (dom B) -head F )
assume A1: F is dom B -headed ; :: thesis: Polish-ext-head F = (dom B) -head F
dom B c= Polish-ext-domain (B,J) by Def9;
hence Polish-ext-head F = (dom B) -head F by A1, POLNOT_1:55; :: thesis: verum