let V be RealLinearSpace; :: thesis: for A being Affine Subset of V st 0. V in A holds
for x being VECTOR of V
for a being Real st x in A holds
a * x in A
let A be Affine Subset of V; :: thesis: ( 0. V in A implies for x being VECTOR of V
for a being Real st x in A holds
a * x in A )
assume A1: 0. V in A ; :: thesis: for x being VECTOR of V
for a being Real st x in A holds
a * x in A
for x being VECTOR of V
for a being Real st x in A holds
a * x in A

proof

let x be VECTOR of V; :: thesis: for a being Real st x in A holds
a * x in A
let a be Real; :: thesis: ( x in A implies a * x in A )
assume x in A ; :: thesis: a * x in A
then ((1 - a) * (0. V)) + (a * x) in A by A1, Def4;
then (0. V) + (a * x) in A ;
hence a * x in A ; :: thesis: verum

end;

hence for x being VECTOR of V
for a being Real st x in A holds
a * x in A ; :: thesis: verum