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 = inf 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 = inf 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 = inf Y ) and

A4: for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & seq2 . n = inf Y ) ; :: thesis: seq1 = seq2

A5: for y being object st y in NAT holds

seq1 . y = seq2 . y

NAT = dom seq1 by FUNCT_2:def 1;

hence seq1 = seq2 by A5, A7, FUNCT_1:2; :: thesis: verum

( Y = { (seq . k) where k is Nat : n <= k } & seq1 . n = inf 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 = inf 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 = inf Y ) and

A4: for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & seq2 . n = inf Y ) ; :: thesis: seq1 = seq2

A5: for y being object st y in NAT holds

seq1 . y = seq2 . y

proof

A7:
NAT = dom seq2
by FUNCT_2:def 1;
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 = inf Z ) by A4;

ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & seq1 . n = inf Y ) by A3;

hence seq1 . y = seq2 . y by A6; :: thesis: verum

end;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 = inf Z ) by A4;

ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & seq1 . n = inf Y ) by A3;

hence seq1 . y = seq2 . y by A6; :: thesis: verum

NAT = dom seq1 by FUNCT_2:def 1;

hence seq1 = seq2 by A5, A7, FUNCT_1:2; :: thesis: verum