theorem Th24: :: ANPROJ10:40

for p, q being Tuple of 1, REAL
for r being Real st p = r * q & p <> <*0*> holds
ex a, b being Real st
( p = <*a*> & q = <*b*> & r = a / b )