theorem Th28: :: NIVEN:30

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