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