for n1, n2, n3 being Element of F_Real
for n, u being Element of (TOP-REAL 3) st n = <*n1,n2,n3*> & u . 3 = 1 holds
|(n,u)| = ((n1 * (u . 1)) + (n2 * (u . 2))) + n3