let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K holds
( V1 is trivial iff dim V1 = 0 )
let V1 be finite-dimensional VectSp of K; :: thesis: ( V1 is trivial iff dim V1 = 0 )

hereby :: thesis: ( dim V1 = 0 implies V1 is trivial )

assume A1: V1 is trivial ; :: thesis: dim V1 = 0
the carrier of V1 c= {(0. V1)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of V1 or x in {(0. V1)} )
assume A2: x in the carrier of V1 ; :: thesis: x in {(0. V1)}
x = 0. V1 by A1, A2;
hence x in {(0. V1)} by TARSKI:def 1; :: thesis: verum

end;

then the carrier of ((Omega). V1) = {(0. V1)} by ZFMISC_1:33
.= the carrier of ((0). V1) by VECTSP_4:def 3 ;
then (Omega). V1 = (0). V1 by VECTSP_4:29;
hence dim V1 = 0 by VECTSP_9:29; :: thesis: verum

end;

assume dim V1 = 0 ; :: thesis: V1 is trivial
then A3: (Omega). V1 = (0). V1 by VECTSP_9:29;
for v1 being Element of V1 holds v1 = 0. V1 by VECTSP_4:35, A3, STRUCT_0:def 5;
hence V1 is trivial ; :: thesis: verum