let F be Field; :: thesis: for V being VectSp of F holds
( V is trivial iff the carrier of V = {(0. V)} )
let V be VectSp of F; :: thesis: ( V is trivial iff the carrier of V = {(0. V)} )
thus ( V is trivial implies the carrier of V = {(0. V)} ) :: thesis: ( the carrier of V = {(0. V)} implies V is trivial )

proof

assume V: V is trivial ; :: thesis: the carrier of V = {(0. V)}

now :: thesis: for y being object st y in the carrier of V holds
y in {(0. V)}

let y be object ; :: thesis: ( y in the carrier of V implies y in {(0. V)} )
assume y in the carrier of V ; :: thesis: y in {(0. V)}
then y = 0. V by V;
hence y in {(0. V)} by TARSKI:def 1; :: thesis: verum

end;

hence the carrier of V = {(0. V)} by TARSKI:def 3; :: thesis: verum

end;

thus ( the carrier of V = {(0. V)} implies V is trivial ) ; :: thesis: verum