let X be RealNormSpace; :: thesis: for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds

Sum R3 = (Sum R1) - (Sum R2)

let R1, R2, R3 be FinSequence of X; :: thesis: ( len R1 = len R2 & R3 = R1 - R2 implies Sum R3 = (Sum R1) - (Sum R2) )

assume A1: ( len R1 = len R2 & R3 = R1 - R2 ) ; :: thesis: Sum R3 = (Sum R1) - (Sum R2)

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)

Sum R3 = (Sum R1) - (Sum R2)

let R1, R2, R3 be FinSequence of X; :: thesis: ( len R1 = len R2 & R3 = R1 - R2 implies Sum R3 = (Sum R1) - (Sum R2) )

assume A1: ( len R1 = len R2 & R3 = R1 - R2 ) ; :: thesis: Sum R3 = (Sum R1) - (Sum R2)

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)

proof

thus
Sum R3 = (Sum R1) - (Sum R2)
by A1, A4, A5, RLVECT_2:5; :: thesis: verum
let k be Nat; :: thesis: ( k in dom R1 implies R3 . k = (R1 /. k) - (R2 /. k) )

assume A6: k in dom R1 ; :: thesis: R3 . k = (R1 /. k) - (R2 /. k)

thus R3 . k = R3 /. k by A6, A3, PARTFUN1:def 6

.= (R1 /. k) - (R2 /. k) by A1, A6, A3, VFUNCT_1:def 2 ; :: thesis: verum

end;assume A6: k in dom R1 ; :: thesis: R3 . k = (R1 /. k) - (R2 /. k)

thus R3 . k = R3 /. k by A6, A3, PARTFUN1:def 6

.= (R1 /. k) - (R2 /. k) by A1, A6, A3, VFUNCT_1:def 2 ; :: thesis: verum