let n be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is non-decreasing & seq is bounded_above holds
( (superior_realsequence seq) . n = sup seq & superior_realsequence seq is V8() )
let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & seq is bounded_above implies ( (superior_realsequence seq) . n = sup seq & superior_realsequence seq is V8() ) )
assume A1: ( seq is non-decreasing & seq is bounded_above ) ; :: thesis: ( (superior_realsequence seq) . n = sup seq & superior_realsequence seq is V8() )
defpred S₁[ Nat] means (superior_realsequence seq) . $1 = sup seq;
for n being Nat holds (superior_realsequence seq) . n = sup seq

proof

A2: S₁[ 0 ] by A1, Th41;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
k in NAT by ORDINAL1:def 13;
hence ( S₁[k] implies S₁[k + 1] ) by A1, Th68; :: thesis: verum

end;

thus for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3); :: thesis: verum

end;

hence ( (superior_realsequence seq) . n = sup seq & superior_realsequence seq is V8() ) by VALUED_0:def 18; :: thesis: verum