let seq be Real_Sequence; :: thesis: ( ( seq is bounded implies for r being Real 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 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 A1: seq is bounded ; :: thesis: for r being Real holds r (#) seq is bounded
let r be Real; :: 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 A1; :: thesis: verum

end;

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

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

end;

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

hence r (#) seq is bounded by A1; :: 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 such that
A2: 0 < r and
A3: for n being Nat holds |.((abs seq) . n).| < r by SEQ_2:3;

now :: thesis: for n being Nat holds |.(seq . n).| < r

let n be Nat; :: thesis: |.(seq . n).| < r
|.((abs seq) . n).| = |.|.(seq . n).|.| by SEQ_1:12
.= |.(seq . n).| ;
hence |.(seq . n).| < r by A3; :: thesis: verum

end;

hence seq is bounded by A2, SEQ_2:3; :: thesis: verum