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