theorem Th16: :: HILBERT3:17

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 (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D))