let f, g be Function; :: thesis: ( f is one-to-one & g is one-to-one implies [:f,g:] " = [:(f " ),(g " ):] )
assume A1: ( f is one-to-one & g is one-to-one ) ; :: thesis: [:f,g:] " = [:(f " ),(g " ):]
then A2: [:f,g:] is one-to-one by ISOCAT_1:1;
A3: ( dom (f " ) = rng f & dom (g " ) = rng g ) by A1, FUNCT_1:55;
A4: dom ([:f,g:] " ) = rng [:f,g:] by A2, FUNCT_1:55
.= [:(dom (f " )),(dom (g " )):] by A3, 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 A5: ( x in dom (f " ) & y in dom (g " ) ) ; :: thesis: ([:f,g:] " ) . x,y = [((f " ) . x),((g " ) . y)]
A6: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 9;
( (f " ) . x in rng (f " ) & (g " ) . y in rng (g " ) ) by A5, FUNCT_1:def 5;
then ( (f " ) . x in dom f & (g " ) . y in dom g ) by A1, FUNCT_1:55;
then A7: [((f " ) . x),((g " ) . y)] in dom [:f,g:] by A6, ZFMISC_1:106;
A8: f " is one-to-one by A1;
A9: f . ((f " ) . x) = (f * (f " )) . x by A5, FUNCT_1:23
.= (((f " ) " ) * (f " )) . x by A1, FUNCT_1:65
.= (id (dom (f " ))) . x by A8, FUNCT_1:61
.= x by A5, FUNCT_1:35 ;
A10: g " is one-to-one by A1;
g . ((g " ) . y) = (g * (g " )) . y by A5, FUNCT_1:23
.= (((g " ) " ) * (g " )) . y by A1, FUNCT_1:65
.= (id (dom (g " ))) . y by A10, FUNCT_1:61
.= y by A5, FUNCT_1:35 ;
then [:f,g:] . ((f " ) . x),((g " ) . y) = [x,y] by A6, A7, A9, FUNCT_3:86;
hence ([:f,g:] " ) . x,y = [((f " ) . x),((g " ) . y)] by A2, A7, FUNCT_1:54; :: thesis: verum

end;

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