set ZS = Rat-Module ;
let s be Element of Rat-Module; :: thesis: Lin {s} <> Rat-Module
assume AS: Lin {s} = Rat-Module ; :: thesis: contradiction
consider m, n being Integer such that
P2: ( n <> 0 & s = m / n ) by RAT_1:1;

per cases ( n = - 1 or n <> - 1 ) ;

suppose N1: n = - 1 ; :: thesis: contradiction

reconsider t = 1 / 2 as Element of Rat-Module by RAT_1:def 1;
t in Lin {s} by AS;
then consider l being Linear_Combination of {s} such that
P3: t = Sum l by ZMODUL02:64;
P4: Sum l = (l . s) * s by ZMODUL02:21;
reconsider k = l . s as Integer ;
1 / 2 = k * (- m) by N1, P2, P3, P4, LMTFRat2
.= - (k * m) ;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose N0: n <> - 1 ; :: thesis: contradiction

per cases ( m = 1 or m = - 1 or ( m <> 1 & m <> - 1 ) ) ;

suppose C1: ( m = 1 or m = - 1 ) ; :: thesis: contradiction

per cases ( m = 1 or m = - 1 ) by C1;

suppose D1: m = 1 ; :: thesis: contradiction

per cases ( n = - 2 or n <> - 2 ) ;

suppose XD3: n = - 2 ; :: thesis: contradiction

reconsider t = - (1 / 3) as Element of Rat-Module by RAT_1:def 2;
t in Lin {s} by AS;
then consider l being Linear_Combination of {s} such that
P3: t = Sum l by ZMODUL02:64;
P4: Sum l = (l . s) * s by ZMODUL02:21;
reconsider k = l . s as Integer ;
P5: - (1 / 3) = k / n by D1, P2, P3, P4, LMTFRat2;
k = (k / n) * n by P2, XCMPLX_1:87
.= 2 / 3 by P5, XD3 ;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose XD2: n <> - 2 ; :: thesis: contradiction

reconsider t = 1 / (n + 1) as Element of Rat-Module by RAT_1:def 1;
t in Lin {s} by AS;
then consider l being Linear_Combination of {s} such that
P3: t = Sum l by ZMODUL02:64;
P4: Sum l = (l . s) * s by ZMODUL02:21;
reconsider k = l . s as Integer ;
P5: 1 / (n + 1) = k / n by D1, P2, P3, P4, LMTFRat2;
k = n / (n + 1) by P2, P5, XCMPLX_1:87;
hence contradiction by LMThFRat31X, N0, XD2, P2; :: thesis: verum

end;

end;

end;

suppose D2: m = - 1 ; :: thesis: contradiction

per cases ( n = - 2 or n <> - 2 ) ;

suppose XD3: n = - 2 ; :: thesis: contradiction

reconsider t = 1 / 3 as Element of Rat-Module by RAT_1:def 1;
t in Lin {s} by AS;
then consider l being Linear_Combination of {s} such that
P3: t = Sum l by ZMODUL02:64;
P4: Sum l = (l . s) * s by ZMODUL02:21;
reconsider k = l . s as Integer ;
P5: 1 / 3 = k * (m / n) by P2, P3, P4, LMTFRat2
.= - (k / n) by D2 ;
k = (k / n) * n by P2, XCMPLX_1:87
.= 2 / 3 by P5, XD3 ;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose XD2: n <> - 2 ; :: thesis: contradiction

reconsider t = (- 1) / (n + 1) as Element of Rat-Module by RAT_1:def 1;
t in Lin {s} by AS;
then consider l being Linear_Combination of {s} such that
P3: t = Sum l by ZMODUL02:64;
P4: Sum l = (l . s) * s by ZMODUL02:21;
reconsider k = l . s as Integer ;
(- 1) / (n + 1) = k * (m / n) by P2, P3, P4, LMTFRat2
.= - (k / n) by D2 ;
then k = n / (n + 1) by P2, XCMPLX_1:87;
hence contradiction by LMThFRat31X, N0, P2, XD2; :: thesis: verum

end;

end;

end;

end;

end;

suppose C2: ( m <> 1 & m <> - 1 ) ; :: thesis: contradiction

reconsider t = (m + 1) / n as Element of Rat-Module by RAT_1:def 1;
t in Lin {s} by AS;
then consider l being Linear_Combination of {s} such that
P3: t = Sum l by ZMODUL02:64;
P4: Sum l = (l . s) * s by ZMODUL02:21;
reconsider k = l . s as Integer ;
P5: (m + 1) / n = k * (m / n) by P2, P3, P4, LMTFRat2;
m + 1 = ((m + 1) / n) * n by P2, XCMPLX_1:87
.= k * ((m / n) * n) by P5
.= k * m by P2, XCMPLX_1:87 ;
then m * (k - 1) = 1 ;
hence contradiction by C2, INT_1:9; :: thesis: verum

end;

end;

end;

end;