theorem :: FUNCT_3:70

for f, g, h, k being Function holds [:f,h:] * <:g,k:> = <:(f * g),(h * k):>