let n be Element of NAT ; :: thesis: for x being Element of REAL n st n >= 2 & x <> 0* n holds
ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y )
let x be Element of REAL n; :: thesis: ( n >= 2 & x <> 0* n implies ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y ) )
assume that
A1: n >= 2 and
A2: x <> 0* n ; :: thesis: ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y )
reconsider f = x as FinSequence of REAL ;
consider i2 being Element of NAT such that
A3: 1 <= i2 and
A4: i2 <= n and
A5: f . i2 <> 0 by A2, Th54;
A6: len f = n by FINSEQ_1:def 18;
then A7: 1 <= len f by A1, XXREAL_0:2;

per cases ( i2 > 1 or i2 <= 1 ) ;

suppose A8: i2 > 1 ; :: thesis: ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y )

reconsider g = <*((f /. 1) + 1)*> ^ (mid f,2,(len f)) as FinSequence of REAL ;
A9: len (mid f,2,(len f)) = ((len f) -' 2) + 1 by A1, A6, A7, FINSEQ_6:124
.= ((len f) - 2) + 1 by A1, A6, XREAL_1:235 ;
len g = (len <*((f /. 1) + 1)*>) + (len (mid f,2,(len f))) by FINSEQ_1:35;
then A10: len g = 1 + (((len f) - 2) + 1) by A9, FINSEQ_1:56
.= len f ;
then reconsider y2 = g as Element of REAL n by A6, Th52;
A11: len <*((f /. 1) + 1)*> = 1 by FINSEQ_1:56;

now

given r being Real such that A12: ( y2 = r * x or x = r * y2 ) ; :: thesis: contradiction

per cases ( y2 = r * x or x = r * y2 ) by A12;

suppose A13: y2 = r * x ; :: thesis: contradiction

i2 <= ((len f) - (1 + 1)) + (1 + 1) by A4, FINSEQ_1:def 18;
then A14: i2 - 1 <= ((((len f) - (1 + 1)) + 1) + 1) - 1 by XREAL_1:11;
A15: ( i2 -' 1 = i2 - 1 & 1 <= i2 -' 1 ) by A8, NAT_D:49, XREAL_1:235;
A16: 1 <= len f by A1, A6, XXREAL_0:2;
then A17: g /. 1 = g . 1 by A10, FINSEQ_4:24;
A18: g /. i2 = g . i2 by A3, A4, A6, A10, FINSEQ_4:24;
A19: ((i2 -' 1) + 2) -' 1 = (((i2 -' 1) + 1) + 1) -' 1
.= (i2 -' 1) + 1 by NAT_D:34
.= (i2 - 1) + 1 by A3, XREAL_1:235
.= i2 ;
A20: f /. i2 = f . i2 by A3, A4, A6, FINSEQ_4:24;
( 1 + 1 <= i2 & i2 <= 1 + (len (mid f,2,(len f))) ) by A4, A8, A9, FINSEQ_1:def 18, NAT_1:13;
then g . i2 = (mid f,2,(len f)) . (i2 - 1) by A11, FINSEQ_1:36
.= f . i2 by A1, A6, A9, A16, A15, A14, A19, FINSEQ_6:124 ;
then 1 * (f /. i2) = r * (f /. i2) by A3, A4, A6, A13, A18, A20, Th53;
then A21: 1 = r by A5, A20, XCMPLX_1:5;
g /. 1 = r * (f /. 1) by A13, A16, Th53;
then (f /. 1) + 1 = 1 * (f /. 1) by A21, A17, FINSEQ_1:58;
hence contradiction ; :: thesis: verum

end;

suppose A22: x = r * y2 ; :: thesis: contradiction

i2 <= ((len f) - (1 + 1)) + (1 + 1) by A4, FINSEQ_1:def 18;
then A23: i2 - 1 <= ((((len f) - (1 + 1)) + 1) + 1) - 1 by XREAL_1:11;
A24: ( i2 -' 1 = i2 - 1 & 1 <= i2 -' 1 ) by A8, NAT_D:49, XREAL_1:235;
A25: 1 <= len f by A1, A6, XXREAL_0:2;
then A26: g /. 1 = g . 1 by A10, FINSEQ_4:24;
A27: g /. i2 = g . i2 by A3, A4, A6, A10, FINSEQ_4:24;
A28: ((i2 -' 1) + 2) -' 1 = (((i2 -' 1) + 1) + 1) -' 1
.= (i2 -' 1) + 1 by NAT_D:34
.= (i2 - 1) + 1 by A3, XREAL_1:235
.= i2 ;
A29: f /. i2 = f . i2 by A3, A4, A6, FINSEQ_4:24;
( 1 + 1 <= i2 & i2 <= 1 + (len (mid f,2,(len f))) ) by A4, A8, A9, FINSEQ_1:def 18, NAT_1:13;
then g . i2 = (mid f,2,(len f)) . (i2 - 1) by A11, FINSEQ_1:36
.= f . i2 by A1, A6, A9, A25, A24, A23, A28, FINSEQ_6:124 ;
then 1 * (f /. i2) = r * (f /. i2) by A3, A4, A6, A10, A22, A27, A29, Th53;
then A30: 1 = r by A5, A29, XCMPLX_1:5;
f /. 1 = r * (g /. 1) by A10, A22, A25, Th53;
then (f /. 1) + 1 = 1 * (f /. 1) by A30, A26, FINSEQ_1:58;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y ) ; :: thesis: verum

end;

suppose A31: i2 <= 1 ; :: thesis: ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y )

reconsider g = (mid f,1,((len f) -' 1)) ^ <*((f /. (len f)) + 1)*> as FinSequence of REAL ;
A32: (len f) -' 1 <= len f by NAT_D:44;
A33: (1 + 1) - 1 <= (len f) - 1 by A1, A6, XREAL_1:11;
A34: (len f) -' 1 = (len f) - 1 by A1, A6, XREAL_1:235, XXREAL_0:2;
then A35: (((len f) -' 1) -' 1) + 1 = (((len f) - 1) - 1) + 1 by A33, XREAL_1:235
.= ((len f) - (1 + 1)) + 1 ;
then A36: len (mid f,1,((len f) -' 1)) = (len f) - 1 by A7, A34, A32, A33, FINSEQ_6:124;
( len <*((f /. (len f)) + 1)*> = 1 & len (mid f,1,((len f) -' 1)) = ((len f) - 2) + 1 ) by A7, A34, A32, A33, A35, FINSEQ_1:56, FINSEQ_6:124;
then A37: len g = (((len f) - 2) + 1) + 1 by FINSEQ_1:35
.= len f ;
then reconsider y2 = g as Element of REAL n by A6, Th52;
A38: i2 = 1 by A3, A31, XXREAL_0:1;

now

given r being Real such that A39: ( y2 = r * x or x = r * y2 ) ; :: thesis: contradiction

per cases ( y2 = r * x or x = r * y2 ) by A39;

suppose A40: y2 = r * x ; :: thesis: contradiction

A41: g /. i2 = g . i2 by A3, A4, A6, A37, FINSEQ_4:24;
A42: f /. i2 = f . i2 by A3, A4, A6, FINSEQ_4:24;
g . i2 = (mid f,1,((len f) -' 1)) . i2 by A38, A33, A36, FINSEQ_6:115
.= f . i2 by A38, A34, A32, A33, FINSEQ_6:129 ;
then 1 * (f /. i2) = r * (f /. i2) by A3, A4, A6, A40, A41, A42, Th53;
then A43: 1 = r by A5, A42, XCMPLX_1:5;
A44: g . (len f) = g . (((len f) - 1) + 1)
.= (f /. (len f)) + 1 by A36, FINSEQ_1:59 ;
A45: 1 <= len f by A1, A6, XXREAL_0:2;
then A46: g /. (len f) = g . (len f) by A37, FINSEQ_4:24;
g /. (len f) = r * (f /. (len f)) by A40, A45, Th53;
hence contradiction by A43, A46, A44; :: thesis: verum

end;

suppose A47: x = r * y2 ; :: thesis: contradiction

A48: g /. i2 = g . i2 by A3, A4, A6, A37, FINSEQ_4:24;
A49: f /. i2 = f . i2 by A3, A4, A6, FINSEQ_4:24;
g . i2 = (mid f,1,((len f) -' 1)) . i2 by A38, A33, A36, FINSEQ_6:115
.= f . i2 by A38, A34, A32, A33, FINSEQ_6:129 ;
then 1 * (f /. i2) = r * (f /. i2) by A3, A4, A6, A37, A47, A48, A49, Th53;
then A50: 1 = r by A5, A49, XCMPLX_1:5;
A51: g . (len f) = g . (((len f) - 1) + 1)
.= (f /. (len f)) + 1 by A36, FINSEQ_1:59 ;
A52: 1 <= len f by A1, A6, XXREAL_0:2;
then A53: g /. (len f) = g . (len f) by A37, FINSEQ_4:24;
f /. (len f) = r * (g /. (len f)) by A37, A47, A52, Th53;
hence contradiction by A50, A53, A51; :: thesis: verum

end;

end;

end;

hence ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y ) ; :: thesis: verum

end;

end;