let V1 be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for F being FinSequence of V1 st ( for k being Nat st k in dom F holds

F /. k = 0. V1 ) holds

Sum F = 0. V1

let F be FinSequence of V1; :: thesis: ( ( for k being Nat st k in dom F holds

F /. k = 0. V1 ) implies Sum F = 0. V1 )

assume A1: for k being Nat st k in dom F holds

F /. k = 0. V1 ; :: thesis: Sum F = 0. V1

defpred S_{1}[ FinSequence of V1] means ( ( for k being Nat st k in dom $1 holds

$1 /. k = 0. V1 ) implies Sum $1 = 0. V1 );

A2: for p being FinSequence of V1

for x being Element of V1 st S_{1}[p] holds

S_{1}[p ^ <*x*>]
_{1}[ <*> the carrier of V1]
by RLVECT_1:43;

for p being FinSequence of V1 holds S_{1}[p]
from FINSEQ_2:sch 2(A11, A2);

hence Sum F = 0. V1 by A1; :: thesis: verum

F /. k = 0. V1 ) holds

Sum F = 0. V1

let F be FinSequence of V1; :: thesis: ( ( for k being Nat st k in dom F holds

F /. k = 0. V1 ) implies Sum F = 0. V1 )

assume A1: for k being Nat st k in dom F holds

F /. k = 0. V1 ; :: thesis: Sum F = 0. V1

defpred S

$1 /. k = 0. V1 ) implies Sum $1 = 0. V1 );

A2: for p being FinSequence of V1

for x being Element of V1 st S

S

proof

A11:
S
let p be FinSequence of V1; :: thesis: for x being Element of V1 st S_{1}[p] holds

S_{1}[p ^ <*x*>]

let x be Element of V1; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*x*>] )

assume A3: ( ( for k being Nat st k in dom p holds

p /. k = 0. V1 ) implies Sum p = 0. V1 ) ; :: thesis: S_{1}[p ^ <*x*>]

A4: (len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:4;

assume A5: for k being Nat st k in dom (p ^ <*x*>) holds

(p ^ <*x*>) /. k = 0. V1 ; :: thesis: Sum (p ^ <*x*>) = 0. V1

A6: for k being Nat st k in dom p holds

p /. k = 0. V1

.= (len p) + 1 by FINSEQ_1:39 ;

then A9: (len p) + 1 in dom (p ^ <*x*>) by A4, FINSEQ_1:def 3;

A10: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42;

thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RLVECT_1:41

.= (Sum p) + x by RLVECT_1:44

.= (Sum p) + ((p ^ <*x*>) /. ((len p) + 1)) by A9, A10, PARTFUN1:def 6

.= (0. V1) + (0. V1) by A3, A5, A6, A9

.= 0. V1 by RLVECT_1:def 4 ; :: thesis: verum

end;S

let x be Element of V1; :: thesis: ( S

assume A3: ( ( for k being Nat st k in dom p holds

p /. k = 0. V1 ) implies Sum p = 0. V1 ) ; :: thesis: S

A4: (len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:4;

assume A5: for k being Nat st k in dom (p ^ <*x*>) holds

(p ^ <*x*>) /. k = 0. V1 ; :: thesis: Sum (p ^ <*x*>) = 0. V1

A6: for k being Nat st k in dom p holds

p /. k = 0. V1

proof

len (p ^ <*x*>) =
(len p) + (len <*x*>)
by FINSEQ_1:22
A7:
dom p c= dom (p ^ <*x*>)
by FINSEQ_1:26;

let k be Nat; :: thesis: ( k in dom p implies p /. k = 0. V1 )

assume A8: k in dom p ; :: thesis: p /. k = 0. V1

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

thus p /. k = p . k by A8, PARTFUN1:def 6

.= (p ^ <*x*>) . k1 by A8, FINSEQ_1:def 7

.= (p ^ <*x*>) /. k by A8, A7, PARTFUN1:def 6

.= 0. V1 by A5, A8, A7 ; :: thesis: verum

end;let k be Nat; :: thesis: ( k in dom p implies p /. k = 0. V1 )

assume A8: k in dom p ; :: thesis: p /. k = 0. V1

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

thus p /. k = p . k by A8, PARTFUN1:def 6

.= (p ^ <*x*>) . k1 by A8, FINSEQ_1:def 7

.= (p ^ <*x*>) /. k by A8, A7, PARTFUN1:def 6

.= 0. V1 by A5, A8, A7 ; :: thesis: verum

.= (len p) + 1 by FINSEQ_1:39 ;

then A9: (len p) + 1 in dom (p ^ <*x*>) by A4, FINSEQ_1:def 3;

A10: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42;

thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RLVECT_1:41

.= (Sum p) + x by RLVECT_1:44

.= (Sum p) + ((p ^ <*x*>) /. ((len p) + 1)) by A9, A10, PARTFUN1:def 6

.= (0. V1) + (0. V1) by A3, A5, A6, A9

.= 0. V1 by RLVECT_1:def 4 ; :: thesis: verum

for p being FinSequence of V1 holds S

hence Sum F = 0. V1 by A1; :: thesis: verum