theorem Th31: :: EUCLID_8:39

for x, y, z being Real holds |[x,y,z]| = ((x * <e1>) + (y * <e2>)) + (z * <e3>)