let X be LinearTopSpace; :: thesis: for r being non zero Real holds mlt (r,X) is continuous
let r be non zero Real; :: thesis: mlt (r,X) is continuous

A1: now

let P be Subset of X; :: thesis: ( P is open implies (mlt (r,X)) " P is open )
defpred S₁[ Subset of X] means ( $1 is open & r * $1 c= P );
consider F being Subset-Family of X such that
A2: for A being Subset of X holds
( A in F iff S₁[A] ) from SUBSET_1:sch 3();
reconsider F = F as Subset-Family of X ;
assume A3: P is open ; :: thesis: (mlt (r,X)) " P is open
A4: union F = (mlt (r,X)) " P

proof

thus union F c= (mlt (r,X)) " P :: according to XBOOLE_0:def 10 :: thesis: (mlt (r,X)) " P c= union F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union F or x in (mlt (r,X)) " P )
assume x in union F ; :: thesis: x in (mlt (r,X)) " P
then consider A being set such that
A5: x in A and
A6: A in F by TARSKI:def 4;
reconsider A = A as Subset of X by A6;
A is Subset of X ;
then reconsider x = x as Point of X by A5;
A7: (mlt (r,X)) . x = r * x by Def13;
( r * A c= P & r * x in r * A ) by A2, A5, A6;
hence x in (mlt (r,X)) " P by A7, FUNCT_2:46; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (mlt (r,X)) " P or x in union F )
assume A8: x in (mlt (r,X)) " P ; :: thesis: x in union F
then reconsider x = x as Point of X ;
(mlt (r,X)) . x in P by A8, FUNCT_2:46;
then r * x in P by Def13;
then consider e being positive Real, W being Subset of X such that
A9: W is open and
A10: x in W and
A11: for s being Real st abs (s - r) < e holds
s * W c= P by A3, Def9;
abs (r - r) < e by ABSVALUE:7;
then r * W c= P by A11;
then W in F by A2, A9;
hence x in union F by A10, TARSKI:def 4; :: thesis: verum

end;

F is open

proof

let A be Subset of X; :: according to TOPS_2:def 1 :: thesis: ( not A in F or A is open )
assume A in F ; :: thesis: A is open
hence A is open by A2; :: thesis: verum

end;

hence (mlt (r,X)) " P is open by A4, TOPS_2:26; :: thesis: verum

end;

[#] X <> {} ;
hence mlt (r,X) is continuous by A1, TOPS_2:55; :: thesis: verum