let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st seq is bounded holds
- seq is bounded
let seq be sequence of X; :: thesis: ( seq is bounded implies - seq is bounded )
assume seq is bounded ; :: thesis: - seq is bounded
then consider M being Real such that
A1: M > 0 and
A2: for n being Nat holds ||.(seq . n).|| <= M ;
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 CSSPACE:47 ;
hence ||.((- seq) . n).|| <= M by A2; :: thesis: verum
end;
hence - seq is bounded by A1; :: thesis: verum