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