let n be Nat; :: thesis: for x being Element of REAL n st |.x.| = 0 holds
x = 0* n
let x be Element of REAL n; :: thesis: ( |.x.| = 0 implies x = 0* n )
assume A1: |.x.| = 0 ; :: thesis: x = 0* n

now :: thesis: for j being Nat st j in Seg n holds
x . j = (n |-> 0) . j

let j be Nat; :: thesis: ( j in Seg n implies x . j = (n |-> 0) . j )
assume j in Seg n ; :: thesis: x . j = (n |-> 0) . j
reconsider r = x . j as Element of REAL by XREAL_0:def 1;
Sum (sqr x) = 0 by A1, RVSUM_1:86, SQUARE_1:24;
then Sum (sqr (abs x)) = 0 by Lm2;
then (abs x) . j = (n |-> 0) . j by RVSUM_1:91;
then |.r.| = (n |-> 0) . j by VALUED_1:18;
then |.r.| = 0 ;
then r = 0 by ABSVALUE:2;
hence x . j = (n |-> 0) . j ; :: thesis: verum

end;

hence x = 0* n by FINSEQ_2:119; :: thesis: verum