let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v being Element of V holds Sum <*v*> = v
let v be Element of V; :: thesis: Sum <*v*> = 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 Def12;
0 < 1 ;
then consider j being Nat such that
A3: j < len <*v*> ;
A4: len <*v*> = 1 by FINSEQ_1:39;
then A5: <*v*> . (j + 1) = <*v*> . (0 + 1) by A3, NAT_1:14
.= v ;
j = 0 by A4, A3, NAT_1:14;
then f . 1 = (0. V) + v by A2, A5
.= v ;
hence Sum <*v*> = v by A1, FINSEQ_1:39; :: thesis: verum