let n be Element of 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 Th38
.= - (upper_bound (- (seq ^\ n))) by A1, Th14, SEQM_3:57
.= - (upper_bound ((- seq) ^\ n)) by SEQM_3:38 ;
hence (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) by Th39; :: thesis: verum