let V be ComplexLinearSpace; :: thesis: for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
let W be Subspace of V; :: thesis: for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
let C be Coset of W; :: thesis: ( 0. V in C iff C = the carrier of W )
ex v being VECTOR of V st C = v + W by Def12;
hence ( 0. V in C iff C = the carrier of W ) by Th66; :: thesis: verum