let X be RealLinearSpace; :: thesis:
let R1, R2, R3 be FinSequence of X; :: thesis:
assume AS: ( len R1 = len R2 & R3 = R1 - R2 ) ; :: thesis:
then P0: dom R1 = dom R2 by FINSEQ_3:31;
P1: dom R3 = (dom R1) /\ (dom R2) by AS, VFUNCT_1:def 2
.= dom R1 by P0 ;
then P2: len R3 = len R1 by FINSEQ_3:31;
for k being Element of NAT st k in dom R1 holds
R3 . k = (R1 /. k) - (R2 /. k)

let k be Element of NAT ; :: thesis:
assume P31: k in dom R1 ; :: thesis:
hence R3 . k = R3 /. k by P1, PARTFUN1:def 8
.= (R1 /. k) - (R2 /. k) by AS, VFUNCT_1:def 2, P31, P1 ;
:: thesis:

end;