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;
per cases ( A = {} or A <> {} ) ;
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;
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 H1( 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 = H1(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
proof
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;
then f is one-to-one by FUNCT_2:19;
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;
end;