theorem Th21: :: EUCLID_8:25

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