:: deftheorem defines SVF1 PDIFF_2:def 1 :
for n, i being Element of NAT
for f being PartFunc of (REAL n),REAL
for z being Element of REAL n holds SVF1 (i,f,z) = f * (reproj (i,z));