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 Th48;

now

let x be Point of X; :: thesis: ((mlt r,X) " ) . x = (mlt (r " ),X) . x
consider u being set such that
A2: u in dom (mlt r,X) and
A3: x = (mlt r,X) . u by A1, FUNCT_1:def 5;
reconsider u = u as Point of X by A2;
A4: x = r * u by A3, Def13;
thus ((mlt r,X) " ) . x = ((mlt r,X) " ) . x by A1, Lm14, TOPS_2:def 4
.= u by A3, Lm14, FUNCT_2:32
.= 1 * u by RLVECT_1:def 11
.= (r * (r " )) * u by XCMPLX_0:def 7
.= (r " ) * x by A4, RLVECT_1:def 10
.= (mlt (r " ),X) . x by Def13 ; :: thesis: verum

end;

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