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 r <> 0 holds

Affin (r * AR) = r * (Affin AR)

let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for AR being Subset of R st r <> 0 holds

Affin (r * AR) = r * (Affin AR)

let AR be Subset of R; :: thesis: ( r <> 0 implies Affin (r * AR) = r * (Affin AR) )

assume A1: r <> 0 ; :: thesis: Affin (r * AR) = r * (Affin AR)

(r ") * (r * AR) = ((r ") * r) * AR by Th10

.= 1 * AR by A1, XCMPLX_0:def 7

.= AR by Th11 ;

then AR c= (r ") * (Affin (r * AR)) by Lm7, Th9;

then A2: Affin AR c= (r ") * (Affin (r * AR)) by Th51, Th54;

r * AR c= r * (Affin AR) by Lm7, Th9;

then A3: Affin (r * AR) c= r * (Affin AR) by Th51, Th54;

r * ((r ") * (Affin (r * AR))) = (r * (r ")) * (Affin (r * AR)) by Th10

.= 1 * (Affin (r * AR)) by A1, XCMPLX_0:def 7

.= Affin (r * AR) by Th11 ;

then r * (Affin AR) c= Affin (r * AR) by A2, Th9;

hence Affin (r * AR) = r * (Affin AR) by A3; :: thesis: verum

for AR being Subset of R st r <> 0 holds

Affin (r * AR) = r * (Affin AR)

let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for AR being Subset of R st r <> 0 holds

Affin (r * AR) = r * (Affin AR)

let AR be Subset of R; :: thesis: ( r <> 0 implies Affin (r * AR) = r * (Affin AR) )

assume A1: r <> 0 ; :: thesis: Affin (r * AR) = r * (Affin AR)

(r ") * (r * AR) = ((r ") * r) * AR by Th10

.= 1 * AR by A1, XCMPLX_0:def 7

.= AR by Th11 ;

then AR c= (r ") * (Affin (r * AR)) by Lm7, Th9;

then A2: Affin AR c= (r ") * (Affin (r * AR)) by Th51, Th54;

r * AR c= r * (Affin AR) by Lm7, Th9;

then A3: Affin (r * AR) c= r * (Affin AR) by Th51, Th54;

r * ((r ") * (Affin (r * AR))) = (r * (r ")) * (Affin (r * AR)) by Th10

.= 1 * (Affin (r * AR)) by A1, XCMPLX_0:def 7

.= Affin (r * AR) by Th11 ;

then r * (Affin AR) c= Affin (r * AR) by A2, Th9;

hence Affin (r * AR) = r * (Affin AR) by A3; :: thesis: verum