let i be natural Number ; :: thesis:
let R be Element of i -tuples_on REAL; :: thesis:
assume A1: Sum (sqr R) = 0 ; :: thesis:
A2: len R = i by CARD_1:def 7;
A3: len (i |-> 0) = i by CARD_1:def 7;
assume R <> i |-> 0 ; :: thesis:
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;
R . j <> 0 by A5;
then 0 < (R . j) ^2 by SQUARE_1:12;
then A7: 0 < (sqr R) . j by VALUED_1:11;

let k be Nat; :: thesis:
assume k in dom (sqr R) ; :: thesis:
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:

end;