for n being Nat st n >= 1 holds
Basel-seq . n = 1 / (n to_power 2)
proof
let n be Nat; :: thesis: ( n >= 1 implies Basel-seq . n = 1 / (n to_power 2) )
assume n >= 1 ; :: thesis: Basel-seq . n = 1 / (n to_power 2)
Basel-seq . n = 1 / (n ^2) by BASEL_1:31
.= 1 / (n to_power 2) by NEWTON:81 ;
hence Basel-seq . n = 1 / (n to_power 2) ; :: thesis: verum
end;
hence Basel-seq is summable by SERIES_1:32; :: thesis: verum