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;
A4: dom (f ") = rng f by A1, FUNCT_1:33;
A5: dom (g ") = rng g by A2, FUNCT_1:33;
A6: dom ([:f,g:] ") = rng [:f,g:] by A3, FUNCT_1:33
.= [:(dom (f ")),(dom (g ")):] by A4, A5, FUNCT_3:67 ;
for x, y being object st x in dom (f ") & y in dom (g ") holds
([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)]

proof

let x, y be object ; :: 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 8;
A10: (f ") . x in rng (f ") by A7, FUNCT_1:def 3;
A11: (g ") . y in rng (g ") by A8, FUNCT_1:def 3;
A12: (f ") . x in dom f by A1, A10, FUNCT_1:33;
(g ") . y in dom g by A2, A11, FUNCT_1:33;
then A13: [((f ") . x),((g ") . y)] in dom [:f,g:] by A9, A12, ZFMISC_1:87;
A14: f . ((f ") . x) = (f * (f ")) . x by A7, FUNCT_1:13
.= (((f ") ") * (f ")) . x by A1, FUNCT_1:43
.= (id (dom (f "))) . x by A1, FUNCT_1:39
.= x by A7, FUNCT_1:18 ;
g . ((g ") . y) = (g * (g ")) . y by A8, FUNCT_1:13
.= (((g ") ") * (g ")) . y by A2, FUNCT_1:43
.= (id (dom (g "))) . y by A2, FUNCT_1:39
.= y by A8, FUNCT_1:18 ;
then [:f,g:] . (((f ") . x),((g ") . y)) = [x,y] by A9, A13, A14, FUNCT_3:65;
hence ([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)] by A1, A2, A13, FUNCT_1:32; :: thesis: verum

end;

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