let V be non empty left_zeroed addLoopStr ; :: thesis: for a being Element of V holds Sum <*a*> = a
let v be Element of V; :: thesis: Sum <*v*> = v
reconsider a = v as Element of V ;
set S = <*v*>;
consider f being Function of NAT ,the carrier of V such that
A1: Sum <*v*> = f . (len <*v*>) and
A2: f . 0 = 0. V and
A3: for j being Element of NAT
for v being Element of V st j < len <*v*> & v = <*v*> . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 13;
A4: len <*a*> = 1 by FINSEQ_1:56;
0 < 1 ;
then consider j being Element of NAT such that
A5: j < len <*v*> by A4;
A6: j = 0 by A4, A5, NAT_1:14;
<*v*> . (j + 1) = <*v*> . (0 + 1) by A4, A5, NAT_1:14
.= v by FINSEQ_1:57 ;
then f . 1 = (0. V) + v by A2, A3, A5, A6
.= a by ALGSTR_1:def 5 ;
hence Sum <*v*> = v by A1, FINSEQ_1:56; :: thesis: verum