let seq1, seq2 be Real_Sequence; :: thesis: ( ( for n being Element of NAT
for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds
seq1 . n = upper_bound Y ) & ( for n being Element of NAT
for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds
seq2 . n = upper_bound Y ) implies seq1 = seq2 )
assume that
A1: for n being Element of NAT
for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds
seq1 . n = sup Y and
A2: for m being Element of NAT
for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : m <= k } holds
seq2 . m = sup Y ; :: thesis: seq1 = seq2
A3: for y being set st y in NAT holds
seq1 . y = seq2 . y

proof

let y be set ; :: thesis: ( y in NAT implies seq1 . y = seq2 . y )
assume y in NAT ; :: thesis: seq1 . y = seq2 . y
then reconsider y = y as Element of NAT ;
reconsider Y = { (seq . k) where k is Element of NAT : y <= k } as Subset of REAL by Th29;
seq1 . y = sup Y by A1;
hence seq1 . y = seq2 . y by A2; :: thesis: verum

end;

( NAT = dom seq1 & NAT = dom seq2 ) by FUNCT_2:def 1;
hence seq1 = seq2 by A3, FUNCT_1:9; :: thesis: verum