let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being FinSequence of the carrier of L st ( for i being Element of NAT st i in dom p holds

p . i = 0. L ) holds

Sum p = 0. L

let p be FinSequence of the carrier of L; :: thesis: ( ( for i being Element of NAT st i in dom p holds

p . i = 0. L ) implies Sum p = 0. L )

assume A1: for k being Element of NAT st k in dom p holds

p . k = 0. L ; :: thesis: Sum p = 0. L

p . i = 0. L ) holds

Sum p = 0. L

let p be FinSequence of the carrier of L; :: thesis: ( ( for i being Element of NAT st i in dom p holds

p . i = 0. L ) implies Sum p = 0. L )

assume A1: for k being Element of NAT st k in dom p holds

p . k = 0. L ; :: thesis: Sum p = 0. L

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

p /. k = 0. L

hence
Sum p = 0. L
by MATRLIN:11; :: thesis: verump /. k = 0. L

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

assume A2: k in dom p ; :: thesis: p /. k = 0. L

hence p /. k = p . k by PARTFUN1:def 6

.= 0. L by A1, A2 ;

:: thesis: verum

end;assume A2: k in dom p ; :: thesis: p /. k = 0. L

hence p /. k = p . k by PARTFUN1:def 6

.= 0. L by A1, A2 ;

:: thesis: verum