for a being Real
for u, v being Element of (TOP-REAL 3) holds
( a * |(u,v)| = |((a * u),v)| & a * |(u,v)| = |(u,(a * v))| )