for X, Y, Z, y being set st y <> {} & y c= Y holds
[:X,y:] * [:Y,Z:] = [:X,Z:] by Lm62;