let q1, q2 be FinSequence of REAL ; :: thesis: ( len q1 = len p & ( for n being Element of NAT st n in dom p holds
q1 /. n = |.(p /. n).| ) & len q2 = len p & ( for n being Element of NAT st n in dom p holds
q2 /. n = |.(p /. n).| ) implies q1 = q2 )
assume that
A5: len q1 = len p and
A6: for n being Element of NAT st n in dom p holds
q1 /. n = |.(p /. n).| and
A7: len q2 = len p and
A8: for n being Element of NAT st n in dom p holds
q2 /. n = |.(p /. n).| ; :: thesis: q1 = q2

A9: now :: thesis: for n being Nat st n in dom p holds
q1 /. n = q2 /. n

let n be Nat; :: thesis: ( n in dom p implies q1 /. n = q2 /. n )
assume A10: n in dom p ; :: thesis: q1 /. n = q2 /. n
hence q1 /. n = |.(p /. n).| by A6
.= q2 /. n by A8, A10 ;
:: thesis: verum

end;

( dom q1 = dom p & dom q2 = dom p ) by A5, A7, FINSEQ_3:29;
hence q1 = q2 by A9, FINSEQ_5:12; :: thesis: verum