let F be real-valued FinSequence; :: thesis: 0 <= Sum (sqr F)

now :: thesis: for i being Nat st i in dom (sqr F) holds
0 <= (sqr F) . i

let i be Nat; :: thesis: ( i in dom (sqr F) implies 0 <= (sqr F) . i )
assume i in dom (sqr F) ; :: thesis: 0 <= (sqr F) . i
0 <= (F . i) ^2 by XREAL_1:63;
hence 0 <= (sqr F) . i by VALUED_1:11; :: thesis: verum

end;

hence 0 <= Sum (sqr F) by Th84; :: thesis: verum