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 ( m = 1 or m = - 1 or ( m <> 1 & m <> - 1 ) ) ;

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

per cases then ( m = 1 or m = - 1 ) ;

suppose D1: m = 1 ; :: 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, P2; :: thesis: verum

end;

suppose D2: m = - 1 ; :: 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, P2; :: thesis: verum

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;