let seq1, seq2 be ExtREAL_sequence; :: thesis: ( ( for n being Nat ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : n <= k } & seq1 . n = sup Y ) ) & ( for n being Nat ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : n <= k } & seq2 . n = sup Y ) ) implies seq1 = seq2 )
assume that
A3: for n being Nat ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : n <= k } & seq1 . n = sup Y ) and
A4: for m being Nat ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : m <= k } & seq2 . m = sup 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 n = y as Element of NAT ;
A6: ex Z being non empty Subset of ExtREAL st
( Z = { (seq . k) where k is Nat : n <= k } & seq2 . n = sup Z ) by A4;
ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : n <= k } & seq1 . n = sup Y ) by A3;
hence seq1 . y = seq2 . y by A6; :: thesis: verum
end;
A7: NAT = dom seq2 by FUNCT_2:def 1;
NAT = dom seq1 by FUNCT_2:def 1;
hence seq1 = seq2 by A5, A7, FUNCT_1:2; :: thesis: verum