for x, y, z being Real
for p being Point of (TOP-REAL 3) st p = |[x,y,z]| holds
( p `1 = x & p `2 = y & p `3 = z ) by FINSEQ_1:45;