let GF be Field; :: thesis: for V being VectSp of GF
for x being Element of V
for A being Subset of V st A = the carrier of V holds
x ++ A = A
let V be VectSp of GF; :: thesis: for x being Element of V
for A being Subset of V st A = the carrier of V holds
x ++ A = A
let x be Element of V; :: thesis: for A being Subset of V st A = the carrier of V holds
x ++ A = A
let A be Subset of V; :: thesis: ( A = the carrier of V implies x ++ A = A )
assume P0: A = the carrier of V ; :: thesis: x ++ A = A
for y being object holds
( y in x ++ A iff y in A )

proof

let y be object ; :: thesis: ( y in x ++ A iff y in A )
( y in A implies y in x ++ A )

proof

assume y in A ; :: thesis: y in x ++ A
then reconsider w = y as Element of V ;
(w - x) + x = w - (x - x) by RLVECT_1:29
.= w - (0. V) by RLVECT_1:15
.= w by RLVECT_1:13 ;
hence y in x ++ A by P0; :: thesis: verum

end;

hence ( y in x ++ A iff y in A ) by P0; :: thesis: verum

end;

hence x ++ A = A by TARSKI:2; :: thesis: verum