let T be Polish-language; :: thesis: for V being full Polish-language of T
for Q being Extension of V
for F being Formula of Q st F is T -headed holds
Polish-ext-head F = T -head F
let V be full Polish-language of T; :: thesis: for Q being Extension of V
for F being Formula of Q st F is T -headed holds
Polish-ext-head F = T -head F
let Q be Extension of V; :: thesis: for F being Formula of Q st F is T -headed holds
Polish-ext-head F = T -head F
let F be Formula of Q; :: thesis: ( F is T -headed implies Polish-ext-head F = T -head F )
assume A1: F is T -headed ; :: thesis: Polish-ext-head F = T -head F
T c= Polish-ext-domain Q by Def9;
hence Polish-ext-head F = T -head F by A1, POLNOT_1:55; :: thesis: verum