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
A3: len q1 = len p and
A4: for n being Element of NAT st n in dom p holds
q1 /. n = |.(p /. n).| and
A5: len q2 = len p and
A6: for n being Element of NAT st n in dom p holds
q2 /. n = |.(p /. n).| ; :: thesis: q1 = q2

A7: now

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

end;

( dom q1 = dom p & dom q2 = dom p ) by A3, A5, FINSEQ_3:31;
hence q1 = q2 by A7, FINSEQ_5:13; :: thesis: verum