let V be free finite-rank Z_Module; :: thesis: ( rank V = 0 iff (Omega). V = (0). V )

consider I being finite Subset of V such that

A1: I is Basis of V by ZMODUL03:def 3;

then Lin I = (0). V by A1, VECTSP_7:def 3;

then ( I = {} or I = {(0. V)} ) by ZMODUL02:68;

hence rank V = 0 by A1, VECTSP_7:def 3, ZMODUL03:def 5, CARD_1:27; :: thesis: verum

consider I being finite Subset of V such that

A1: I is Basis of V by ZMODUL03:def 3;

hereby :: thesis: ( (Omega). V = (0). V implies rank V = 0 )

assume
(Omega). V = (0). V
; :: thesis: rank V = 0 consider I being finite Subset of V such that

A2: I is Basis of V by ZMODUL03:def 3;

assume rank V = 0 ; :: thesis: (Omega). V = (0). V

then card I = 0 by A2, ZMODUL03:def 5;

then A3: I = {} the carrier of V ;

(Omega). V = Lin I by A2, VECTSP_7:def 3

.= (0). V by A3, ZMODUL02:67 ;

hence (Omega). V = (0). V ; :: thesis: verum

end;A2: I is Basis of V by ZMODUL03:def 3;

assume rank V = 0 ; :: thesis: (Omega). V = (0). V

then card I = 0 by A2, ZMODUL03:def 5;

then A3: I = {} the carrier of V ;

(Omega). V = Lin I by A2, VECTSP_7:def 3

.= (0). V by A3, ZMODUL02:67 ;

hence (Omega). V = (0). V ; :: thesis: verum

then Lin I = (0). V by A1, VECTSP_7:def 3;

then ( I = {} or I = {(0. V)} ) by ZMODUL02:68;

hence rank V = 0 by A1, VECTSP_7:def 3, ZMODUL03:def 5, CARD_1:27; :: thesis: verum