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 A2, PARTFUN1:def 6;
then A5: y = r * (f /. x) by A2, A4, VFUNCT_1:def 4;
f . x = f /. x by A1, A2, PARTFUN1:def 6;
then f /. x in f .: X by A1, A2, A3, FUNCT_1:def 6;
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 A7, FUNCT_1:def 6;
v = f /. x by A8, A10, PARTFUN1:def 6;
then y = (r (#) f) /. x by A1, A6, A8, VFUNCT_1:def 4
.= (r (#) f) . x by A1, A8, PARTFUN1:def 6 ;
hence y in (r (#) f) .: X by A1, A8, A9, FUNCT_1:def 6; :: thesis: verum