let V be free Z_Module; :: thesis: ( [#] V is finite implies (Omega). V = (0). V )

assume A1: [#] V is finite ; :: thesis: (Omega). V = (0). V

assume A2: (Omega). V <> (0). V ; :: thesis: contradiction

consider A being Subset of V such that

a3: A is base by VECTSP_7:def 4;

assume A1: [#] V is finite ; :: thesis: (Omega). V = (0). V

assume A2: (Omega). V <> (0). V ; :: thesis: contradiction

consider A being Subset of V such that

a3: A is base by VECTSP_7:def 4;

per cases
( A = {} or A <> {} )
;

end;

suppose
A = {}
; :: thesis: contradiction

then Lin A =
Lin ({} the carrier of V)

.= (0). V by VECTSP_7:9 ;

hence contradiction by A2, a3; :: thesis: verum

end;.= (0). V by VECTSP_7:9 ;

hence contradiction by A2, a3; :: thesis: verum

suppose
A <> {}
; :: thesis: contradiction

then consider v being object such that

A4: v in A by XBOOLE_0:def 1;

reconsider v = v as VECTOR of V by A4;

{v} is linearly-independent by a3, A4, ZFMISC_1:31, ZMODUL02:56;

then A5: v <> 0. V ;

deffunc H_{1}( Element of INT.Ring) -> Element of the carrier of V = $1 * v;

consider f being Function of the carrier of INT.Ring, the carrier of V such that

A6: for x being Element of INT.Ring holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

A7: ( dom f = the carrier of INT.Ring & rng f c= the carrier of V ) by FUNCT_2:def 1;

for x1, x2 being object st x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & f . x1 = f . x2 holds

x1 = x2

then card the carrier of INT.Ring c= card the carrier of V by A7, CARD_1:10;

hence contradiction by A1; :: thesis: verum

end;A4: v in A by XBOOLE_0:def 1;

reconsider v = v as VECTOR of V by A4;

{v} is linearly-independent by a3, A4, ZFMISC_1:31, ZMODUL02:56;

then A5: v <> 0. V ;

deffunc H

consider f being Function of the carrier of INT.Ring, the carrier of V such that

A6: for x being Element of INT.Ring holds f . x = H

A7: ( dom f = the carrier of INT.Ring & rng f c= the carrier of V ) by FUNCT_2:def 1;

for x1, x2 being object st x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & f . x1 = f . x2 holds

x1 = x2

proof

then
f is one-to-one
by FUNCT_2:19;
let x1, x2 be object ; :: thesis: ( x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & f . x1 = f . x2 implies x1 = x2 )

assume A8: ( x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & f . x1 = f . x2 ) ; :: thesis: x1 = x2

then reconsider a1 = x1, a2 = x2 as Element of INT.Ring ;

a1 * v = f . a2 by A6, A8

.= a2 * v by A6 ;

then (a1 * v) - (a2 * v) = 0. V by RLVECT_1:5;

then (a1 - a2) * v = 0. V by ZMODUL01:9;

then a1 - a2 = 0. INT.Ring by A5, ZMODUL01:def 7;

hence x1 = x2 by INT_3:def 3; :: thesis: verum

end;assume A8: ( x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & f . x1 = f . x2 ) ; :: thesis: x1 = x2

then reconsider a1 = x1, a2 = x2 as Element of INT.Ring ;

a1 * v = f . a2 by A6, A8

.= a2 * v by A6 ;

then (a1 * v) - (a2 * v) = 0. V by RLVECT_1:5;

then (a1 - a2) * v = 0. V by ZMODUL01:9;

then a1 - a2 = 0. INT.Ring by A5, ZMODUL01:def 7;

hence x1 = x2 by INT_3:def 3; :: thesis: verum

then card the carrier of INT.Ring c= card the carrier of V by A7, CARD_1:10;

hence contradiction by A1; :: thesis: verum