theorem Th23: :: EUCLID_8:27

for r being Real holds r * <e3> = |[0,0,r]|