theorem Th2: :: PDIFF_8:2

for x being Real
for vx being Element of (REAL-NS 1) st vx = <*x*> holds
||.vx.|| = |.x.|