theorem :: FUNCT_3:56

for A being set
for f, g being Function holds <:f,g:> .: A c= [:(f .: A),(g .: A):]