let X be LinearTopSpace; for r being non zero Real holds (mlt (r,X)) " = mlt ((r "),X)
let r be non zero Real; (mlt (r,X)) " = mlt ((r "),X)
A1:
rng (mlt (r,X)) = [#] X
by Th47;
now for x being Point of X holds ((mlt (r,X)) ") . x = (mlt ((r "),X)) . xlet x be
Point of
X;
((mlt (r,X)) ") . x = (mlt ((r "),X)) . xconsider 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
;
verum end;
hence
(mlt (r,X)) " = mlt ((r "),X)
by FUNCT_2:63; verum