let R be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being non empty right_complementable Abelian add-associative right_zeroed ModuleStr over R

for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being 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 ModuleStr over R; :: thesis: for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being 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 V; :: thesis: ( len F = len G & len F = len H & ( for k being 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 and

A2: len F = len H and

A3: for k being Nat st k in dom F holds

H . k = (F /. k) - (G /. k) ; :: thesis: Sum H = (Sum F) - (Sum G)

deffunc H_{1}( Nat) -> Element of the carrier of V = - (G /. $1);

consider I being FinSequence such that

A4: len I = len G and

A5: for k being Nat st k in dom I holds

I . k = H_{1}(k)
from FINSEQ_1:sch 2();

A6: dom I = Seg (len G) by A4, FINSEQ_1:def 3;

then A7: for k being Nat st k in Seg (len G) holds

I . k = H_{1}(k)
by A5;

rng I c= the carrier of V

A10: Seg (len G) = dom G by FINSEQ_1:def 3;

Sum I = - (Sum G) by A4, A7, A10, Th4;

hence Sum H = (Sum F) - (Sum G) by A14; :: thesis: verum

for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being 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 ModuleStr over R; :: thesis: for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being 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 V; :: thesis: ( len F = len G & len F = len H & ( for k being 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 and

A2: len F = len H and

A3: for k being Nat st k in dom F holds

H . k = (F /. k) - (G /. k) ; :: thesis: Sum H = (Sum F) - (Sum G)

deffunc H

consider I being FinSequence such that

A4: len I = len G and

A5: for k being Nat st k in dom I holds

I . k = H

A6: dom I = Seg (len G) by A4, FINSEQ_1:def 3;

then A7: for k being Nat st k in Seg (len G) holds

I . k = H

rng I c= the carrier of V

proof

then reconsider I = I as FinSequence of V by FINSEQ_1:def 4;
let x be object ; :: 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 object such that

A8: y in dom I and

A9: I . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A8;

x = - (G /. y) by A5, A8, A9;

then reconsider v = x as Element of V ;

v in V ;

hence x in the carrier of V ; :: thesis: verum

end;assume x in rng I ; :: thesis: x in the carrier of V

then consider y being object such that

A8: y in dom I and

A9: I . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A8;

x = - (G /. y) by A5, A8, A9;

then reconsider v = x as Element of V ;

v in V ;

hence x in the carrier of V ; :: thesis: verum

A10: Seg (len G) = dom G by FINSEQ_1:def 3;

now :: thesis: for k being Nat st k in dom F holds

H . k = (F /. k) + (I /. k)

then A14:
Sum H = (Sum F) + (Sum I)
by A1, A2, A4, Th2;H . k = (F /. k) + (I /. k)

let k be Nat; :: thesis: ( k in dom F implies H . k = (F /. k) + (I /. k) )

A11: dom F = dom G by A1, FINSEQ_3:29;

assume A12: k in dom F ; :: thesis: H . k = (F /. k) + (I /. k)

then k in dom I by A1, A4, FINSEQ_3:29;

then A13: I . k = I /. k by PARTFUN1:def 6;

thus H . k = (F /. k) - (G /. k) by A3, A12

.= (F /. k) + (- (G /. k))

.= (F /. k) + (I /. k) by A5, A6, A10, A12, A13, A11 ; :: thesis: verum

end;A11: dom F = dom G by A1, FINSEQ_3:29;

assume A12: k in dom F ; :: thesis: H . k = (F /. k) + (I /. k)

then k in dom I by A1, A4, FINSEQ_3:29;

then A13: I . k = I /. k by PARTFUN1:def 6;

thus H . k = (F /. k) - (G /. k) by A3, A12

.= (F /. k) + (- (G /. k))

.= (F /. k) + (I /. k) by A5, A6, A10, A12, A13, A11 ; :: thesis: verum

Sum I = - (Sum G) by A4, A7, A10, Th4;

hence Sum H = (Sum F) - (Sum G) by A14; :: thesis: verum