theorem :: FUNCT_3:80

for A, B, C being non empty set
for f, g being Function of A,[:B,C:] st (pr1 (B,C)) * f = (pr1 (B,C)) * g & (pr2 (B,C)) * f = (pr2 (B,C)) * g holds
f = g