let f, g be Function; :: thesis: [:f,g:] = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):>
A1: dom (pr1 ((dom f),(dom g))) = [:(dom f),(dom g):] by Def4;
A2: dom (pr2 ((dom f),(dom g))) = [:(dom f),(dom g):] by Def5;
rng (pr2 ((dom f),(dom g))) c= dom g by Th45;
then A3: dom (g * (pr2 ((dom f),(dom g)))) = [:(dom f),(dom g):] by A2, RELAT_1:27;
rng (pr1 ((dom f),(dom g))) c= dom f by Th43;
then dom (f * (pr1 ((dom f),(dom g)))) = [:(dom f),(dom g):] by A1, RELAT_1:27;
then A4: dom <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> = [:(dom f),(dom g):] by A3, Th50;
A5: for x, y being object st x in dom f & y in dom g holds
[:f,g:] . (x,y) = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> . (x,y)

proof

let x, y be object ; :: thesis: ( x in dom f & y in dom g implies [:f,g:] . (x,y) = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> . (x,y) )
assume A6: ( x in dom f & y in dom g ) ; :: thesis: [:f,g:] . (x,y) = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> . (x,y)
then A7: [x,y] in [:(dom f),(dom g):] by ZFMISC_1:87;
thus [:f,g:] . (x,y) = [(f . x),(g . y)] by A6, Def8
.= [(f . ((pr1 ((dom f),(dom g))) . (x,y))),(g . y)] by A6, Def4
.= [(f . ((pr1 ((dom f),(dom g))) . (x,y))),(g . ((pr2 ((dom f),(dom g))) . (x,y)))] by A6, Def5
.= [((f * (pr1 ((dom f),(dom g)))) . (x,y)),(g . ((pr2 ((dom f),(dom g))) . (x,y)))] by A1, A7, FUNCT_1:13
.= [((f * (pr1 ((dom f),(dom g)))) . (x,y)),((g * (pr2 ((dom f),(dom g)))) . (x,y))] by A2, A7, FUNCT_1:13
.= <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> . (x,y) by A4, A7, Def7 ; :: thesis: verum

end;

dom [:f,g:] = [:(dom f),(dom g):] by Def8;
hence [:f,g:] = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> by A4, A5, Th6; :: thesis: verum