set fP = v tohilbperm ;
set fV = v tohilbval ;

B0: now :: thesis: dom (v tohilbperm) = NAT

(dom (v tohilbperm)) \+\ NAT = {} ;
hence dom (v tohilbperm) = NAT by FOMODEL0:29; :: thesis: verum

end;

now :: thesis: for n being Element of NAT holds (v tohilbperm) . n is Permutation of ((v tohilbval) . n)

let n be Element of NAT ; :: thesis: (v tohilbperm) . n is Permutation of ((v tohilbval) . n)
D0: ( (v tohilbperm) . n = (v . n) tohilb & (v tohilbval) . n = dom ((v . n) tohilb) ) by Lm34;
then reconsider y = (v tohilbperm) . n as symmetric Function ;
( dom y = (v tohilbval) . n & rng y = dom y ) by D0, Lm37;
then y is onto Function of ((v tohilbval) . n),((v tohilbval) . n) by FOMODEL0:75;
hence (v tohilbperm) . n is Permutation of ((v tohilbval) . n) ; :: thesis: verum

end;

hence v tohilbperm is Permutation of v tohilbval by HILBERT3:def 4, B0; :: thesis: verum