let X be LinearTopSpace; :: thesis: for r being non zero Real holds (mlt (r,X)) " = mlt ((r "),X)
let r be non zero Real; :: thesis: (mlt (r,X)) " = mlt ((r "),X)
A1: rng (mlt (r,X)) = [#] X by Th47;

now :: thesis: for x being Point of X holds ((mlt (r,X)) ") . x = (mlt ((r "),X)) . x

let x be Point of X; :: thesis: ((mlt (r,X)) ") . x = (mlt ((r "),X)) . x
consider u being object such that
A2: u in dom (mlt (r,X)) and
A3: x = (mlt (r,X)) . u by A1, FUNCT_1:def 3;
reconsider u = u as Point of X by A2;
A4: x = r * u by A3, Def13;
( mlt (r,X) is onto & mlt (r,X) is one-to-one ) by A1, Lm13, FUNCT_2:def 3;
hence ((mlt (r,X)) ") . x = ((mlt (r,X)) ") . x by TOPS_2:def 4
.= u by A3, Lm13, FUNCT_2:26
.= 1 * u by RLVECT_1:def 8
.= (r * (r ")) * u by XCMPLX_0:def 7
.= (r ") * x by A4, RLVECT_1:def 7
.= (mlt ((r "),X)) . x by Def13 ;
:: thesis: verum

end;

hence (mlt (r,X)) " = mlt ((r "),X) by FUNCT_2:63; :: thesis: verum