let seq1, seq2 be ExtREAL_sequence; :: thesis: ( ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = inf Y ) ) & ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = inf Y ) ) implies seq1 = seq2 )
assume that
A2: for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = inf Y ) and
A3: for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = inf Y ) ; :: thesis: seq1 = seq2
A4: 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 n = y as Element of NAT ;
( ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = inf Y ) & ex Z being non empty Subset of ExtREAL st
( Z = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = inf Z ) ) by A2, A3;
hence seq1 . y = seq2 . y ; :: thesis: verum

end;

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