let A, B be non empty set ; :: thesis: 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))
let C, D be set ; :: thesis: for f being Function of C,A
for g being Function of D,B holds (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D))
let f be Function of C,A; :: thesis: for g being Function of D,B holds (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D))
let g be Function of D,B; :: thesis: (pr2 (A,B)) * [:f,g:] = g * (pr2 (C,D))
( not C = {} or A = {} or [:C,D:] = {} ) ;
then reconsider F = f * (pr1 (C,D)) as Function of [:C,D:],A ;
( not D = {} or A = {} or [:C,D:] = {} ) ;
then reconsider G = g * (pr2 (C,D)) as Function of [:C,D:],B ;
thus (pr2 (A,B)) * [:f,g:] = (pr2 (A,B)) * <:F,G:> by FUNCT_3:77
.= g * (pr2 (C,D)) by FUNCT_3:62 ; :: thesis: verum