theorem Th22: :: EUCLID_8:26

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