theorem Th4: :: BASEL_2:4

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