let seq1, seq2 be Real_Sequence; :: thesis: ( ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
seq1 . n = lower_bound Y ) & ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
seq2 . n = lower_bound Y ) implies seq1 = seq2 )
assume that
A3: for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
seq1 . n = lower_bound Y and
A4: for m being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : m <= k } holds
seq2 . m = lower_bound Y ; :: thesis: seq1 = seq2
A5: for y being object st y in NAT holds
seq1 . y = seq2 . y

proof

let y be object ; :: 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 Nat : y <= k } as Subset of REAL by Th29;
seq1 . y = lower_bound Y by A3;
hence seq1 . y = seq2 . y by A4; :: thesis: verum

end;

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