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 sequence of the carrier of V such that
A1: Sum <*v*> = f . (len <*v*>) and
A2: ( f . 0 = 0. V & ( for j being 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 12;
A3: len <*a*> = 1 by FINSEQ_1:39;
0 < 1 ;
then consider j being Element of NAT such that
A4: j < len <*v*> ;
A5: <*v*> . (j + 1) = <*v*> . (0 + 1) by A3, A4, NAT_1:14
.= v ;
j = 0 by A3, A4, NAT_1:14;
then f . 1 = (0. V) + v by A2, A5
.= a by ALGSTR_1:def 2 ;
hence Sum <*v*> = v by A1, FINSEQ_1:39; :: thesis: verum