let p1, p2 be FinSequence of ExtREAL ; :: thesis: ( dom p1 = dom F & ( for n being Element of NAT st n in dom p1 holds
p1 . n = (F . n) . x ) & dom p2 = dom F & ( for n being Element of NAT st n in dom p2 holds
p2 . n = (F . n) . x ) implies p1 = p2 )
assume that
A4: dom p1 = dom F and
A5: for n being Element of NAT st n in dom p1 holds
p1 . n = (F . n) . x and
A6: dom p2 = dom F and
A7: for n being Element of NAT st n in dom p2 holds
p2 . n = (F . n) . x ; :: thesis: p1 = p2
B1: len p1 = len p2 by A4, A6, FINSEQ_3:29;

now :: thesis: for n being Nat st n in dom p1 holds
p1 . n = p2 . n

let n be Nat; :: thesis: ( n in dom p1 implies p1 . n = p2 . n )
assume A10: n in dom p1 ; :: thesis: p1 . n = p2 . n
then p1 . n = (F . n) . x by A5;
hence p1 . n = p2 . n by A4, A6, A7, A10; :: thesis: verum

end;

hence p1 = p2 by B1, FINSEQ_2:9; :: thesis: verum