let f, g be Function; :: thesis: ( f is one-to-one & g is one-to-one implies [:f,g:] " = [:(f " ),(g " ):] )
assume that
A1: f is one-to-one and
A2: g is one-to-one ; :: thesis: [:f,g:] " = [:(f " ),(g " ):]
A3: [:f,g:] is one-to-one by A1, A2, ISOCAT_1:1;
A4: dom (f " ) = rng f by A1, FUNCT_1:55;
A5: dom (g " ) = rng g by A2, FUNCT_1:55;
A6: dom ([:f,g:] " ) = rng [:f,g:] by A3, FUNCT_1:55
.= [:(dom (f " )),(dom (g " )):] by A4, A5, FUNCT_3:88 ;
for x, y being set st x in dom (f " ) & y in dom (g " ) holds
([:f,g:] " ) . x,y = [((f " ) . x),((g " ) . y)]

proof

let x, y be set ; :: thesis: ( x in dom (f " ) & y in dom (g " ) implies ([:f,g:] " ) . x,y = [((f " ) . x),((g " ) . y)] )
assume that
A7: x in dom (f " ) and
A8: y in dom (g " ) ; :: thesis: ([:f,g:] " ) . x,y = [((f " ) . x),((g " ) . y)]
A9: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 9;
A10: (f " ) . x in rng (f " ) by A7, FUNCT_1:def 5;
A11: (g " ) . y in rng (g " ) by A8, FUNCT_1:def 5;
A12: (f " ) . x in dom f by A1, A10, FUNCT_1:55;
(g " ) . y in dom g by A2, A11, FUNCT_1:55;
then A13: [((f " ) . x),((g " ) . y)] in dom [:f,g:] by A9, A12, ZFMISC_1:106;
A14: f . ((f " ) . x) = (f * (f " )) . x by A7, FUNCT_1:23
.= (((f " ) " ) * (f " )) . x by A1, FUNCT_1:65
.= (id (dom (f " ))) . x by A1, FUNCT_1:61
.= x by A7, FUNCT_1:35 ;
g . ((g " ) . y) = (g * (g " )) . y by A8, FUNCT_1:23
.= (((g " ) " ) * (g " )) . y by A2, FUNCT_1:65
.= (id (dom (g " ))) . y by A2, FUNCT_1:61
.= y by A8, FUNCT_1:35 ;
then [:f,g:] . ((f " ) . x),((g " ) . y) = [x,y] by A9, A13, A14, FUNCT_3:86;
hence ([:f,g:] " ) . x,y = [((f " ) . x),((g " ) . y)] by A3, A13, FUNCT_1:54; :: thesis: verum

end;

hence [:f,g:] " = [:(f " ),(g " ):] by A6, FUNCT_3:def 9; :: thesis: verum