theorem :: AFINSQ_1:37

for x, y, z being object holds
( <%x,y,z%> = <%x%> ^ <%y,z%> & <%x,y,z%> = <%x,y%> ^ <%z%> ) by Th25;