set f = arity-from-list B;
consider a being object such that
A1: a in T and
A2: for b being object st b in dom B holds
not a in B . b by Th59;
for n being Nat holds not a in B . n

proof

given n being Nat such that A3: a in B . n ; :: thesis: contradiction
n in dom B by A3, FUNCT_1:def 2;
hence contradiction by A2, A3; :: thesis: verum

end;

then (arity-from-list B) . a = 0 by Th30, A1;
hence arity-from-list B is Polish-arity-function of T by A1, Def18; :: thesis: verum