let r be Real; :: thesis: for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R st AR is Affine holds
r * AR is Affine
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for AR being Subset of R st AR is Affine holds
r * AR is Affine
let AR be Subset of R; :: thesis: ( AR is Affine implies r * AR is Affine )
assume A1: AR is Affine ; :: thesis: r * AR is Affine
let v1, v2 be VECTOR of R; :: according to RUSUB_4:def 5 :: thesis: for b₁ being Element of REAL holds
( not v1 in r * AR or not v2 in r * AR or ((1 - b₁) * v1) + (b₁ * v2) in r * AR )
let s be Real; :: thesis: ( not v1 in r * AR or not v2 in r * AR or ((1 - s) * v1) + (s * v2) in r * AR )
assume v1 in r * AR ; :: thesis: ( not v2 in r * AR or ((1 - s) * v1) + (s * v2) in r * AR )
then consider w1 being Element of R such that
A2: v1 = r * w1 and
A3: w1 in AR ;
assume v2 in r * AR ; :: thesis: ((1 - s) * v1) + (s * v2) in r * AR
then consider w2 being Element of R such that
A4: v2 = r * w2 and
A5: w2 in AR ;
A6: ((1 - s) * w1) + (s * w2) in AR by A1, A3, A5, RUSUB_4:def 5;
A7: (1 - s) * (r * w1) = ((1 - s) * r) * w1 by RLVECT_1:def 10, RLVECT_1:def 11
.= r * ((1 - s) * w1) by RLVECT_1:def 10, RLVECT_1:def 11 ;
s * (r * w2) = (s * r) * w2 by RLVECT_1:def 10, RLVECT_1:def 11
.= r * (s * w2) by RLVECT_1:def 10, RLVECT_1:def 11 ;
then ((1 - s) * v1) + (s * v2) = r * (((1 - s) * w1) + (s * w2)) by A2, A4, A7, RLVECT_1:def 8;
hence ((1 - s) * v1) + (s * v2) in r * AR by A6; :: thesis: verum