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 CARD_1:def 7;
A3: len (i |-> 0) = i by CARD_1:def 7;
assume R <> i |-> 0 ; :: thesis: contradiction
then consider j being Nat such that
A4: j in dom R and
A5: R . j <> (i |-> 0) . j by A2, A3, FINSEQ_2:9;
set x = R . j;
set x9 = (sqr R) . j;
A6: dom R = Seg (len R) by FINSEQ_1:def 3;
then R . j <> 0 by A2, A4, A5, FUNCOP_1:7;
then 0 < (R . j) ^2 by SQUARE_1:12;
then A7: 0 < (sqr R) . j by VALUED_1:11;

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:63;
hence 0 <= (sqr R) . k by VALUED_1:11; :: thesis: verum

end;

dom (sqr R) = Seg (len (sqr R)) by FINSEQ_1:def 3;
then j in dom (sqr R) by A4, A6, FINSEQ_2:33;
hence contradiction by A1, A8, A7, Th115; :: thesis: verum