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 Element of NAT holds ||.(seq . n).|| <= M by Def10;

now

let n be Element of NAT ; :: thesis: ||.((- seq) . n).|| <= M
||.((- seq) . n).|| = ||.(- (seq . n)).|| by BHSP_1:def 10
.= ||.(seq . n).|| by CSSPACE:49 ;
hence ||.((- seq) . n).|| <= M by A2; :: thesis: verum

end;

hence - seq is bounded by A1, Def10; :: thesis: verum