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 4 :: thesis: for b_{1} being object holds

( not v1 in r * AR or not v2 in r * AR or ((1 - b_{1}) * v1) + (b_{1} * 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;

A7: (1 - s) * (r * w1) = ((1 - s) * r) * w1 by RLVECT_1:def 7

.= r * ((1 - s) * w1) by RLVECT_1:def 7 ;

s * (r * w2) = (s * r) * w2 by RLVECT_1:def 7

.= r * (s * w2) by RLVECT_1:def 7 ;

then ((1 - s) * v1) + (s * v2) = r * (((1 - s) * w1) + (s * w2)) by A2, A4, A7, RLVECT_1:def 5;

hence ((1 - s) * v1) + (s * v2) in r * AR by A6; :: thesis: verum

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 4 :: thesis: for b

( not v1 in r * AR or not v2 in r * AR or ((1 - b

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;

A7: (1 - s) * (r * w1) = ((1 - s) * r) * w1 by RLVECT_1:def 7

.= r * ((1 - s) * w1) by RLVECT_1:def 7 ;

s * (r * w2) = (s * r) * w2 by RLVECT_1:def 7

.= r * (s * w2) by RLVECT_1:def 7 ;

then ((1 - s) * v1) + (s * v2) = r * (((1 - s) * w1) + (s * w2)) by A2, A4, A7, RLVECT_1:def 5;

hence ((1 - s) * v1) + (s * v2) in r * AR by A6; :: thesis: verum