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 Def5;
A2: dom (pr2 (dom f),(dom g)) = [:(dom f),(dom g):] by Def6;
rng (pr2 (dom f),(dom g)) c= dom g by Th61;
then A3: dom (g * (pr2 (dom f),(dom g))) = [:(dom f),(dom g):] by A2, RELAT_1:46;
rng (pr1 (dom f),(dom g)) c= dom f by Th59;
then dom (f * (pr1 (dom f),(dom g))) = [:(dom f),(dom g):] by A1, RELAT_1:46;
then A4: dom <:(f * (pr1 (dom f),(dom g))),(g * (pr2 (dom f),(dom g))):> = [:(dom f),(dom g):] by A3, Th70;
A5: for x, y being set 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 set ; :: 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:106;
thus [:f,g:] . x,y = [(f . x),(g . y)] by A6, Def9
.= [(f . ((pr1 (dom f),(dom g)) . x,y)),(g . y)] by A6, Def5
.= [(f . ((pr1 (dom f),(dom g)) . x,y)),(g . ((pr2 (dom f),(dom g)) . x,y))] by A6, Def6
.= [((f * (pr1 (dom f),(dom g))) . x,y),(g . ((pr2 (dom f),(dom g)) . x,y))] by A1, A7, FUNCT_1:23
.= [((f * (pr1 (dom f),(dom g))) . x,y),((g * (pr2 (dom f),(dom g))) . x,y)] by A2, A7, FUNCT_1:23
.= <:(f * (pr1 (dom f),(dom g))),(g * (pr2 (dom f),(dom g))):> . x,y by A4, A7, Def8 ; :: thesis: verum

end;

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