theorem Th8: :: CAYLDICK:8

for a being Element of N_Real holds a * a = ||.a.|| ^2