let i be Nat; :: thesis: for R being Element of i -tuples_on REAL st Sum (sqr R) = 0 holds
R = i |-> 0
let R be Element of i -tuples_on REAL ; :: thesis: ( Sum (sqr R) = 0 implies R = i |-> 0 )
assume A1: Sum (sqr R) = 0 ; :: thesis: R = i |-> 0
A2: len R = i by FINSEQ_1:def 18;
A3: len (i |-> 0 ) = i by FINSEQ_1:def 18;
assume R <> i |-> 0 ; :: thesis: contradiction
then consider j being Nat such that
A5: j in dom R and
A6: R . j <> (i |-> 0 ) . j by A2, A3, FINSEQ_2:10;
A7: ( dom (sqr R) = Seg (len (sqr R)) & dom R = Seg (len R) ) by FINSEQ_1:def 3;

A8: now

let k be Nat; :: thesis: ( k in dom (sqr R) implies 0 <= (sqr R) . k )
assume k in dom (sqr R) ; :: thesis: 0 <= (sqr R) . k
set r = (sqr R) . k;
set x = R . k;
0 <= (R . k) ^2 by XREAL_1:65;
hence 0 <= (sqr R) . k by VALUED_1:11; :: thesis: verum

end;

A9: j in dom (sqr R) by A5, A7, FINSEQ_2:37;
set x = R . j;
set x' = (sqr R) . j;
R . j <> 0 by A2, A5, A6, A7, FUNCOP_1:13;
then 0 < (R . j) ^2 by SQUARE_1:74;
then 0 < (sqr R) . j by VALUED_1:11;
hence contradiction by A1, A8, A9, Th115; :: thesis: verum