let B be Polish-arity-function; :: thesis: for Z being B -closed Polish-language
for p, q being FinSequence st p in dom B & B . p = 1 & q in Z holds
p ^ q in Z
let Z be B -closed Polish-language; :: thesis: for p, q being FinSequence st p in dom B & B . p = 1 & q in Z holds
p ^ q in Z
let p, q be FinSequence; :: thesis: ( p in dom B & B . p = 1 & q in Z implies p ^ q in Z )
assume that
A1: ( p in dom B & B . p = 1 ) and
A2: q in Z ; :: thesis: p ^ q in Z
A3: q in Z ^^ 1 by A2;
Z is B -closed ;
hence p ^ q in Z by A1, A3; :: thesis: verum