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

end;

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