let x, y be Element of (TOP-REAL 1); :: thesis: for a, b, r being Real st x = <*a*> & y = <*b*> holds
( x = r * y iff a = r * b )
let a, b, r be Real; :: thesis: ( x = <*a*> & y = <*b*> implies ( x = r * y iff a = r * b ) )
assume that
A1: x = <*a*> and
A2: y = <*b*> ; :: thesis: ( x = r * y iff a = r * b )
reconsider rb = r * b as Real ;

hereby :: thesis: ( a = r * b implies x = r * y )

assume x = r * y ; :: thesis: a = r * b
then x = <*rb*> by A2, Th27;
hence a = r * b by A1, FINSEQ_1:76; :: thesis: verum

end;

assume a = r * b ; :: thesis: x = r * y
hence x = r * y by A2, A1, Th27; :: thesis: verum