let r be Real; :: thesis: for V being non empty RLSStruct
for A being non empty set
for f being PartFunc of A, the carrier of V
for X being set holds (r (#) f) .: X = r * (f .: X)

let V be non empty RLSStruct ; :: thesis: for A being non empty set
for f being PartFunc of A, the carrier of V
for X being set holds (r (#) f) .: X = r * (f .: X)

let A be non empty set ; :: thesis: for f being PartFunc of A, the carrier of V
for X being set holds (r (#) f) .: X = r * (f .: X)

let f be PartFunc of A, the carrier of V; :: thesis: for X being set holds (r (#) f) .: X = r * (f .: X)
let X be set ; :: thesis: (r (#) f) .: X = r * (f .: X)
set rf = r (#) f;
A1: dom (r (#) f) = dom f by VFUNCT_1:def 4;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: r * (f .: X) c= (r (#) f) .: X
let y be object ; :: thesis: ( y in (r (#) f) .: X implies y in r * (f .: X) )
assume y in (r (#) f) .: X ; :: thesis: y in r * (f .: X)
then consider x being object such that
A2: x in dom (r (#) f) and
A3: x in X and
A4: y = (r (#) f) . x by FUNCT_1:def 6;
(r (#) f) . x = (r (#) f) /. x by ;
then A5: y = r * (f /. x) by ;
f . x = f /. x by ;
then f /. x in f .: X by ;
then y in { (r * v) where v is Element of V : v in f .: X } by A5;
hence y in r * (f .: X) by CONVEX1:def 1; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in r * (f .: X) or y in (r (#) f) .: X )
assume y in r * (f .: X) ; :: thesis: y in (r (#) f) .: X
then y in { (r * v) where v is Element of V : v in f .: X } by CONVEX1:def 1;
then consider v being Element of V such that
A6: y = r * v and
A7: v in f .: X ;
consider x being object such that
A8: x in dom f and
A9: x in X and
A10: v = f . x by ;
v = f /. x by ;
then y = (r (#) f) /. x by
.= (r (#) f) . x by ;
hence y in (r (#) f) .: X by ; :: thesis: verum