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