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

for a being Real st x in A holds

a * x in A ; :: thesis: verum

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

hence
for x being VECTOR of V
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;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

for a being Real st x in A holds

a * x in A ; :: thesis: verum