let n be Element of 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 seq is bounded_above ; :: thesis: (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)
then A1: ( - seq is bounded_below & seq ^\ n is bounded_above ) by Th26;
(superior_realsequence seq) . n = sup (seq ^\ n) by Th39
.= - (inf (- (seq ^\ n))) by A1, Th13
.= - (inf ((- seq) ^\ n)) by SEQM_3:38 ;
hence (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) by Th38; :: thesis: verum