theorem Th1: :: COMPUT_1:1

for x, y, z being set holds
( <*x,y*> +* (1,z) = <*z,y*> & <*x,y*> +* (2,z) = <*x,z*> )