let n be Nat; :: thesis: for seq being Real_Sequence st seq is bounded_above holds
(superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)
let seq be Real_Sequence; :: thesis: ( seq is bounded_above implies (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) )
assume A1: seq is bounded_above ; :: thesis: (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)
(superior_realsequence seq) . n = upper_bound (seq ^\ n) by Th37
.= - (lower_bound (- (seq ^\ n))) by A1, Th13, SEQM_3:27
.= - (lower_bound ((- seq) ^\ n)) by SEQM_3:16 ;
hence (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) by Th36; :: thesis: verum