theorem Th15: :: HILBERT3:16

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