let seq be Real_Sequence; :: thesis: ( ( seq is bounded implies for r being real number holds r (#) seq is bounded ) & ( seq is bounded implies - seq is bounded ) & ( seq is bounded implies abs seq is bounded ) & ( abs seq is bounded implies seq is bounded ) )
thus ( seq is bounded implies for r being real number holds r (#) seq is bounded ) :: thesis: ( ( seq is bounded implies - seq is bounded ) & ( seq is bounded implies abs seq is bounded ) & ( abs seq is bounded implies seq is bounded ) )

proof

assume Z: seq is bounded ; :: thesis: for r being real number holds r (#) seq is bounded
let r be real number ; :: thesis: r (#) seq is bounded

per cases ( 0 < r or 0 = r or r < 0 ) ;

suppose 0 < r ; :: thesis: r (#) seq is bounded

hence r (#) seq is bounded by Z; :: thesis: verum

end;

suppose 0 = r ; :: thesis: r (#) seq is bounded

hence r (#) seq is bounded by Th68; :: thesis: verum

end;

suppose r < 0 ; :: thesis: r (#) seq is bounded

hence r (#) seq is bounded by Z; :: thesis: verum

end;

end;

end;

thus ( seq is bounded implies - seq is bounded ) ; :: thesis: ( ( seq is bounded implies abs seq is bounded ) & ( abs seq is bounded implies seq is bounded ) )
thus ( seq is bounded implies abs seq is bounded ) ; :: thesis: ( abs seq is bounded implies seq is bounded )
assume abs seq is bounded ; :: thesis: seq is bounded
then consider r being real number such that
A9: ( 0 < r & ( for n being Element of NAT holds abs ((abs seq) . n) < r ) ) by SEQ_2:15;

now

let n be Element of NAT ; :: thesis: abs (seq . n) < r
abs ((abs seq) . n) = abs (abs (seq . n)) by SEQ_1:16
.= abs (seq . n) ;
hence abs (seq . n) < r by A9; :: thesis: verum

end;

hence seq is bounded by A9, SEQ_2:15; :: thesis: verum