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 ;
A5: 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 A3;
ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = inf Y ) by A2;
hence seq1 . y = seq2 . y by A5; :: thesis: verum

end;

A6: NAT = dom seq2 by FUNCT_2:def 1;
NAT = dom seq1 by FUNCT_2:def 1;
hence seq1 = seq2 by A4, A6, FUNCT_1:2; :: thesis: verum