theorem Th29: :: NIVEN:31

for L being non empty right_zeroed addLoopStr
for z0, z1, z2, z3, z4, z5 being Element of L holds <%z0,z1,z2%> + <%z3,z4,z5%> = <%(z0 + z3),(z1 + z4),(z2 + z5)%>