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 (pr1 A,B) * [:f,g:] = f * (pr1 C,D)
let C, D be set ; :: thesis: for f being Function of C,A
for g being Function of D,B holds (pr1 A,B) * [:f,g:] = f * (pr1 C,D)
let f be Function of C,A; :: thesis: for g being Function of D,B holds (pr1 A,B) * [:f,g:] = f * (pr1 C,D)
let g be Function of D,B; :: thesis: (pr1 A,B) * [:f,g:] = f * (pr1 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 (pr1 A,B) * [:f,g:] = (pr1 A,B) * <:F,G:> by FUNCT_3:98
.= f * (pr1 C,D) by FUNCT_3:82 ; :: thesis: verum