let r be Real; 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 ; 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 ; 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; for X being set holds (r (#) f) .: X = r * (f .: X)
let X be set ; (r (#) f) .: X = r * (f .: X)
set rf = r (#) f;
A1:
dom (r (#) f) = dom f
by VFUNCT_1:def 4;
let y be object ; TARSKI:def 3 ( not y in r * (f .: X) or y in (r (#) f) .: X )
assume
y in r * (f .: X)
; 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; verum