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;

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

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 ; :: according to TARSKI:def 3 :: thesis: ( not y in r * (f .: X) or y in (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;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

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