let n be Nat; :: thesis: for s, s1, s2 being Real_Sequence st ( for n being Nat holds s . n = ((s1 . n) + (s2 . n)) ^2 ) holds
(Partial_Sums s) . n >= 0
let s, s1, s2 be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = ((s1 . n) + (s2 . n)) ^2 ) implies (Partial_Sums s) . n >= 0 )
assume A1: for n being Nat holds s . n = ((s1 . n) + (s2 . n)) ^2 ; :: thesis: (Partial_Sums s) . n >= 0

now :: thesis: for n being Nat holds s . n >= 0

let n be Nat; :: thesis: s . n >= 0
s . n = ((s1 . n) + (s2 . n)) ^2 by A1;
hence s . n >= 0 by XREAL_1:63; :: thesis: verum

end;

hence (Partial_Sums s) . n >= 0 by Th34; :: thesis: verum