let q, q1, q2 be FinSequence of REAL ; :: thesis:
assume that
A1: len q1 = len q and
A2: len q1 = len q2 and
A3: for k being Nat st k in dom q1 holds
q . k = (q1 . k) + (q2 . k) ; :: thesis:
for k being Element of NAT st k in dom q1 holds
q . k = (q1 /. k) + (q2 /. k)

let k be Element of NAT ; :: thesis:
assume A4: k in dom q1 ; :: thesis:
A5: k in dom q2 by A2, A4, FINSEQ_3:29;
thus q . k = (q1 . k) + (q2 . k) by A3, A4
.= (q1 /. k) + (q2 . k) by A4, PARTFUN1:def 6
.= (q1 /. k) + (q2 /. k) by A5, PARTFUN1:def 6 ; :: thesis:

end;