let n be Nat; :: thesis: Reci-TSq . n >= 0

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: Reci-TSq . n >= 0

hence Reci-TSq . n >= 0 by MySum2Def; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: Reci-TSq . n >= 0

then reconsider nn = n as non zero Nat ;
Reci-TSq . n = 1 / (TSqF nn) by MySum2Def;
hence Reci-TSq . n >= 0 ; :: thesis: verum

end;

end;