consider M being Real such that
A1: M > 0 and
A2: for n being Nat holds ||.(seq . n).|| <= M by Def3;
now :: thesis: for n being Nat holds ||.((- seq) . n).|| <= M
let n be Nat; :: thesis: ||.((- seq) . n).|| <= M
||.((- seq) . n).|| = ||.(- (seq . n)).|| by BHSP_1:44
.= ||.(seq . n).|| by BHSP_1:31 ;
hence ||.((- seq) . n).|| <= M by A2; :: thesis: verum
end;
hence - seq is bounded by A1; :: thesis: verum