let V be Z_Module; :: thesis: Lin ({} the carrier of V) = (0). V
set A = Lin ({} the carrier of V);

now :: thesis: for v being VECTOR of V holds
( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )

let v be VECTOR of V; :: thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )
thus ( v in Lin ({} the carrier of V) implies v in (0). V ) :: thesis: ( v in (0). V implies v in Lin ({} the carrier of V) )

proof

assume v in Lin ({} the carrier of V) ; :: thesis: v in (0). V
then A1: v in the carrier of (Lin ({} the carrier of V)) ;
the carrier of (Lin ({} the carrier of V)) = { (Sum l0) where l0 is Z_Linear_Combination of {} the carrier of V : verum } by Def37;
then ex l0 being Z_Linear_Combination of {} the carrier of V st v = Sum l0 by A1;
then v = 0. V by Th20;
hence v in (0). V by Th66; :: thesis: verum

end;

assume v in (0). V ; :: thesis: v in Lin ({} the carrier of V)
then v = 0. V by Th66;
hence v in Lin ({} the carrier of V) by ZMODUL01:33; :: thesis: verum

end;

hence Lin ({} the carrier of V) = (0). V by ZMODUL01:46; :: thesis: verum