let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for A being Subset of V holds Affin (v + A) = v + (Affin A)
let v be VECTOR of V; :: thesis: for A being Subset of V holds Affin (v + A) = v + (Affin A)
let A be Subset of V; :: thesis: Affin (v + A) = v + (Affin A)
v + A c= v + (Affin A) by Lm7, RLTOPSP1:8;
then A1: Affin (v + A) c= v + (Affin A) by Th51, RUSUB_4:31;
(- v) + (v + A) = ((- v) + v) + A by Th5
.= (0. V) + A by RLVECT_1:5
.= A by Th6 ;
then A c= (- v) + (Affin (v + A)) by Lm7, RLTOPSP1:8;
then A2: Affin A c= (- v) + (Affin (v + A)) by Th51, RUSUB_4:31;
v + ((- v) + (Affin (v + A))) = (v + (- v)) + (Affin (v + A)) by Th5
.= (0. V) + (Affin (v + A)) by RLVECT_1:5
.= Affin (v + A) by Th6 ;
then v + (Affin A) c= Affin (v + A) by A2, RLTOPSP1:8;
hence Affin (v + A) = v + (Affin A) by A1; :: thesis: verum