theorem Th21: :: EUCLID_4:21

for n being Nat
for x1, x2 being Element of REAL n
for a being Real holds |((a * x1),x2)| = a * |(x1,x2)|