let X be RealNormSpace; :: thesis:
let R1, R2, R3 be FinSequence of X; :: thesis:
assume A1: ( len R1 = len R2 & R3 = R1 - R2 ) ; :: thesis:
then A2: dom R1 = dom R2 by FINSEQ_3:29;
A3: dom R3 = (dom R1) /\ (dom R2) by A1, VFUNCT_1:def 2
.= dom R1 by A2 ;
then A4: len R3 = len R1 by FINSEQ_3:29;
A5: for k being Nat st k in dom R1 holds
R3 . k = (R1 /. k) - (R2 /. k)

let k be Nat; :: thesis:
assume A6: k in dom R1 ; :: thesis:
thus R3 . k = R3 /. k by A6, A3, PARTFUN1:def 6
.= (R1 /. k) - (R2 /. k) by A1, A6, A3, VFUNCT_1:def 2 ; :: thesis:

end;