theorem :: HILBERT3:30

for n being Element of NAT
for V being SetValuation holds SetVal (V,(prop n)) = V . n by Def2;