let r be Real; :: thesis: for V being RealLinearSpace
for A being Subset of V holds Affin (r * A) = r * (Affin A)
let V be RealLinearSpace; :: thesis: for A being Subset of V holds Affin (r * A) = r * (Affin A)
let A be Subset of V; :: thesis: Affin (r * A) = r * (Affin A)
per cases ( r = 0 or r <> 0 ) ;
suppose A1: r = 0 ; :: thesis: Affin (r * A) = r * (Affin A)
then A2: r * (Affin A) c= {(0. V)} by Th12;
A3: r * (Affin A) c= r * A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (Affin A) or x in r * A )
assume A4: x in r * (Affin A) ; :: thesis: x in r * A
then ex v being Element of V st
( x = r * v & v in Affin A ) ;
then not A is empty ;
then consider v being object such that
A5: v in A ;
reconsider v = v as Element of V by A5;
A6: r * v in r * A by A5;
x = 0. V by A2, A4, TARSKI:def 1;
hence x in r * A by A1, A6, RLVECT_1:10; :: thesis: verum
end;
r * A c= {(0. V)} by A1, Th12;
then A7: ( r * A is empty or r * A = {(0. V)} ) by ZFMISC_1:33;
{(0. V)} is Affine by RUSUB_4:23;
then A8: Affin (r * A) = r * A by A7, Lm8;
r * A c= r * (Affin A) by Lm7, Th9;
hence Affin (r * A) = r * (Affin A) by A3, A8; :: thesis: verum
end;
suppose r <> 0 ; :: thesis: Affin (r * A) = r * (Affin A)
hence Affin (r * A) = r * (Affin A) by Th55; :: thesis: verum
end;
end;