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:77

.= f * (pr1 (C,D)) by FUNCT_3:62 ; :: thesis: verum

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:77

.= f * (pr1 (C,D)) by FUNCT_3:62 ; :: thesis: verum