let V be ComplexLinearSpace; :: thesis:
let v be VECTOR of V; :: thesis:
let W be Subspace of V; :: thesis:
( 0. V in W & v + (0. V) = v ) by Th36, RLVECT_1:4;
then A1: v in { (v + u) where u is VECTOR of V : u in W } ;
thus ( v in W implies v + W = the carrier of W ) :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in v + W ; :: thesis:
then consider u being VECTOR of V such that
A3: x = v + u and
A4: u in W ;
v + u in W by A2, A4, Th39;
hence x in the carrier of W by A3; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier of W ; :: thesis:
then reconsider y = x, z = v as Element of W by A2;
reconsider y1 = y, z1 = z as VECTOR of V by Th29;
A5: z + (y - z) = (y + z) - z by RLVECT_1:def 3
.= y + (z - z) by RLVECT_1:def 3
.= y + (0. W) by RLVECT_1:15
.= x by RLVECT_1:4 ;
y - z in W ;
then A6: y1 - z1 in W by Th35;
y - z = y1 - z1 by Th35;
then z1 + (y1 - z1) = x by A5, Th32;
hence x in v + W by A6; :: thesis:

end;