dom A = T by FUNCT_2:def 1;
hence ( P is A -closed iff for p being FinSequence
for n being Nat
for q being FinSequence st p in T & n = A . p & q in P ^^ n holds
p ^ q in P ) ; :: thesis: verum