theorem Th23: :: ANPROJ10:37

for T being RealLinearSpace
for x, y being Element of T
for a being Real
for p, q being Tuple of 1, REAL st T = TOP-REAL 1 & p = x & q = y & x = a * y holds
p = a * q