let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for V being non empty right_complementable Abelian add-associative right_zeroed VectSpStr of R
for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
let V be non empty right_complementable Abelian add-associative right_zeroed VectSpStr of R; :: thesis: for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
let F, G, H be FinSequence of the carrier of V; :: thesis: ( len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) implies Sum H = (Sum F) - (Sum G) )
assume that
A1: ( len F = len G & len F = len H ) and
A2: for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ; :: thesis: Sum H = (Sum F) - (Sum G)
deffunc H₁( Nat) -> Element of the carrier of V = - (G /. $1);
consider I being FinSequence such that
A3: len I = len G and
A4: for k being Nat st k in dom I holds
I . k = H₁(k) from FINSEQ_1:sch 2();
A5: dom I = Seg (len G) by A3, FINSEQ_1:def 3;
A6: for k being Element of NAT st k in Seg (len G) holds
I . k = H₁(k) by A4, A5;
A7: Seg (len G) = dom G by FINSEQ_1:def 3;
rng I c= the carrier of V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng I or x in the carrier of V )
assume x in rng I ; :: thesis: x in the carrier of V
then consider y being set such that
A8: ( y in dom I & I . y = x ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A8;
x = - (G /. y) by A4, A8;
then reconsider v = x as Element of V ;
v in V by RLVECT_1:3;
hence x in the carrier of V ; :: thesis: verum

end;

then reconsider I = I as FinSequence of the carrier of V by FINSEQ_1:def 4;
A9: Sum I = - (Sum G) by A3, A6, A7, RLVECT_2:6;

now

let k be Element of NAT ; :: thesis: ( k in dom F implies H . k = (F /. k) + (I /. k) )
assume A10: k in dom F ; :: thesis: H . k = (F /. k) + (I /. k)
then k in dom I by A1, A3, FINSEQ_3:31;
then A11: I . k = I /. k by PARTFUN1:def 8;
A12: dom F = dom G by A1, FINSEQ_3:31;
thus H . k = (F /. k) - (G /. k) by A2, A10
.= (F /. k) + (- (G /. k)) by RLVECT_1:def 12
.= (F /. k) + (I /. k) by A4, A7, A10, A11, A12, A5 ; :: thesis: verum

end;

then Sum H = (Sum F) + (Sum I) by A1, A3, RLVECT_2:4;
hence Sum H = (Sum F) - (Sum G) by A9, RLVECT_1:def 12; :: thesis: verum