let n be Nat; :: thesis: for x1, x2 being Element of REAL n st x1 <> x2 holds

|.(x1 - x2).| <> 0

let x1, x2 be Element of REAL n; :: thesis: ( x1 <> x2 implies |.(x1 - x2).| <> 0 )

|.(x1 - x2).| <> 0

let x1, x2 be Element of REAL n; :: thesis: ( x1 <> x2 implies |.(x1 - x2).| <> 0 )

now :: thesis: ( x1 <> x2 implies |.(x1 - x2).| <> 0 )

hence
( x1 <> x2 implies |.(x1 - x2).| <> 0 )
; :: thesis: verumassume that

A1: x1 <> x2 and

A2: not |.(x1 - x2).| <> 0 ; :: thesis: contradiction

|((x1 - x2),(x1 - x2))| = 0 ^2 by A2, EUCLID_2:4;

then x1 - x2 = 0* n by Th17;

then x1 = x1 - (x1 + (- x2)) by RVSUM_1:32

.= (x1 - x1) - (- x2) by RVSUM_1:39

.= (0* n) - (- x2) by RVSUM_1:37

.= x2 by RVSUM_1:33 ;

hence contradiction by A1; :: thesis: verum

end;A1: x1 <> x2 and

A2: not |.(x1 - x2).| <> 0 ; :: thesis: contradiction

|((x1 - x2),(x1 - x2))| = 0 ^2 by A2, EUCLID_2:4;

then x1 - x2 = 0* n by Th17;

then x1 = x1 - (x1 + (- x2)) by RVSUM_1:32

.= (x1 - x1) - (- x2) by RVSUM_1:39

.= (0* n) - (- x2) by RVSUM_1:37

.= x2 by RVSUM_1:33 ;

hence contradiction by A1; :: thesis: verum