theorem :: PRELAMB:27

for s being SynTypes_Calculus
for x, y, z being type of s holds <*(x * (y /" z))*> ==>. (x * y) /" z