let n be 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, Th33;
A6: len f = n by CARD_1:def 7;
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 f11 = (f /. 1) + 1 as Element of REAL by XREAL_0:def 1;
reconsider g = <*f11*> ^ (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:118
.= ((len f) - 2) + 1 by A1, A6, XREAL_1:233 ;
len g = (len <*((f /. 1) + 1)*>) + (len (mid (f,2,(len f)))) by FINSEQ_1:22;
then A10: len g = 1 + (((len f) - 2) + 1) by A9, FINSEQ_1:39
.= len f ;
then reconsider y2 = g as Element of REAL n by A6, EUCLID:76;
A11: len <*((f /. 1) + 1)*> = 1 by FINSEQ_1:39;

now :: thesis: for r being Real holds
( not y2 = r * x & not x = r * y2 )

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, CARD_1:def 7;
then A14: i2 - 1 <= ((((len f) - (1 + 1)) + 1) + 1) - 1 by XREAL_1:9;
A15: ( i2 -' 1 = i2 - 1 & 1 <= i2 -' 1 ) by A8, NAT_D:49, XREAL_1:233;
A16: 1 <= len f by A1, A6, XXREAL_0:2;
then A17: g /. 1 = g . 1 by A10, FINSEQ_4:15;
A18: g /. i2 = g . i2 by A3, A4, A6, A10, FINSEQ_4:15;
A19: ((i2 -' 1) + 2) -' 1 = (((i2 -' 1) + 1) + 1) -' 1
.= (i2 -' 1) + 1 by NAT_D:34
.= (i2 - 1) + 1 by A3, XREAL_1:233
.= i2 ;
A20: f /. i2 = f . i2 by A3, A4, A6, FINSEQ_4:15;
( 1 + 1 <= i2 & i2 <= 1 + (len (mid (f,2,(len f)))) ) by A4, A8, A9, CARD_1:def 7, NAT_1:13;
then g . i2 = (mid (f,2,(len f))) . (i2 - 1) by A11, FINSEQ_1:23
.= f . i2 by A1, A6, A9, A16, A15, A14, A19, FINSEQ_6:118 ;
then 1 * (f /. i2) = r * (f /. i2) by A3, A4, A6, A13, A18, A20, Th32;
then A21: 1 = r by A5, A20, XCMPLX_1:5;
g /. 1 = r * (f /. 1) by A13, A16, Th32;
then (f /. 1) + 1 = 1 * (f /. 1) by A21, A17, FINSEQ_1:41;
hence contradiction ; :: thesis: verum

end;

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

i2 <= ((len f) - (1 + 1)) + (1 + 1) by A4, CARD_1:def 7;
then A23: i2 - 1 <= ((((len f) - (1 + 1)) + 1) + 1) - 1 by XREAL_1:9;
A24: ( i2 -' 1 = i2 - 1 & 1 <= i2 -' 1 ) by A8, NAT_D:49, XREAL_1:233;
A25: 1 <= len f by A1, A6, XXREAL_0:2;
then A26: g /. 1 = g . 1 by A10, FINSEQ_4:15;
A27: g /. i2 = g . i2 by A3, A4, A6, A10, FINSEQ_4:15;
A28: ((i2 -' 1) + 2) -' 1 = (((i2 -' 1) + 1) + 1) -' 1
.= (i2 -' 1) + 1 by NAT_D:34
.= (i2 - 1) + 1 by A3, XREAL_1:233
.= i2 ;
A29: f /. i2 = f . i2 by A3, A4, A6, FINSEQ_4:15;
( 1 + 1 <= i2 & i2 <= 1 + (len (mid (f,2,(len f)))) ) by A4, A8, A9, CARD_1:def 7, NAT_1:13;
then g . i2 = (mid (f,2,(len f))) . (i2 - 1) by A11, FINSEQ_1:23
.= f . i2 by A1, A6, A9, A25, A24, A23, A28, FINSEQ_6:118 ;
then 1 * (f /. i2) = r * (f /. i2) by A3, A4, A6, A10, A22, A27, A29, Th32;
then A30: 1 = r by A5, A29, XCMPLX_1:5;
f /. 1 = r * (g /. 1) by A10, A22, A25, Th32;
then (f /. 1) + 1 = 1 * (f /. 1) by A30, A26, FINSEQ_1:41;
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 ff1 = (f /. (len f)) + 1 as Element of REAL by XREAL_0:def 1;
reconsider g = (mid (f,1,((len f) -' 1))) ^ <*ff1*> 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:9;
A34: (len f) -' 1 = (len f) - 1 by A1, A6, XREAL_1:233, XXREAL_0:2;
then A35: (((len f) -' 1) -' 1) + 1 = (((len f) - 1) - 1) + 1 by A33, XREAL_1:233
.= ((len f) - (1 + 1)) + 1 ;
then A36: len (mid (f,1,((len f) -' 1))) = (len f) - 1 by A7, A34, A32, A33, FINSEQ_6:118;
( 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:39, FINSEQ_6:118;
then A37: len g = (((len f) - 2) + 1) + 1 by FINSEQ_1:22
.= len f ;
then reconsider y2 = g as Element of REAL n by A6, EUCLID:76;
A38: i2 = 1 by A3, A31, XXREAL_0:1;

now :: thesis: for r being Real holds
( not y2 = r * x & not x = r * y2 )

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:15;
A42: f /. i2 = f . i2 by A3, A4, A6, FINSEQ_4:15;
g . i2 = (mid (f,1,((len f) -' 1))) . i2 by A38, A33, A36, FINSEQ_6:109
.= f . i2 by A38, A34, A32, A33, FINSEQ_6:123 ;
then 1 * (f /. i2) = r * (f /. i2) by A3, A4, A6, A40, A41, A42, Th32;
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:42 ;
A45: 1 <= len f by A1, A6, XXREAL_0:2;
then A46: g /. (len f) = g . (len f) by A37, FINSEQ_4:15;
g /. (len f) = r * (f /. (len f)) by A40, A45, Th32;
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:15;
A49: f /. i2 = f . i2 by A3, A4, A6, FINSEQ_4:15;
g . i2 = (mid (f,1,((len f) -' 1))) . i2 by A38, A33, A36, FINSEQ_6:109
.= f . i2 by A38, A34, A32, A33, FINSEQ_6:123 ;
then 1 * (f /. i2) = r * (f /. i2) by A3, A4, A6, A37, A47, A48, A49, Th32;
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:42 ;
A52: 1 <= len f by A1, A6, XXREAL_0:2;
then A53: g /. (len f) = g . (len f) by A37, FINSEQ_4:15;
f /. (len f) = r * (g /. (len f)) by A37, A47, A52, Th32;
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;