:: deftheorem defines unitvector PDIFF_4:def 8 :
for a being Element of REAL 3 holds unitvector a = |[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]|;