let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds
( |.(x1 - x2).| = 0 iff x1 = x2 )
let x1, x2 be Element of REAL n; :: thesis: ( |.(x1 - x2).| = 0 iff x1 = x2 )
reconsider R1 = x1, R2 = x2 as Element of n -tuples_on REAL ;
thus ( |.(x1 - x2).| = 0 implies x1 = x2 ) :: thesis: ( x1 = x2 implies |.(x1 - x2).| = 0 )

proof

assume |.(x1 - x2).| = 0 ; :: thesis: x1 = x2
then R1 - R2 = 0* n by Th5
.= n |-> 0 ;
hence x1 = x2 by RVSUM_1:38; :: thesis: verum

end;

assume x1 = x2 ; :: thesis: |.(x1 - x2).| = 0
then R1 - R2 = 0* n by RVSUM_1:37;
hence |.(x1 - x2).| = 0 by Th4; :: thesis: verum