let h1, h2 be Function; :: thesis: ( ( for z being set holds
( z in dom h1 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) ) & ( for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
h1 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ) & ( for z being set holds
( z in dom h2 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) ) & ( for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
h2 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ) implies h1 = h2 )
assume that
A26: for z being set holds
( z in dom h1 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) and
A27: for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
h1 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] and
A28: for z being set holds
( z in dom h2 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) and
A29: for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
h2 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ; :: thesis: h1 = h2
A30: for z being set st z in dom h1 holds
h1 . z = h2 . z

proof

let z be set ; :: thesis: ( z in dom h1 implies h1 . z = h2 . z )
assume z in dom h1 ; :: thesis: h1 . z = h2 . z
then consider x, y, x', y' being set such that
A31: z = [[x,x'],[y,y']] and
A32: ( [x,y] in dom f & [x',y'] in dom g ) by A26;
h1 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] by A27, A32
.= h2 . [x,x'],[y,y'] by A29, A32 ;
hence h1 . z = h2 . z by A31; :: thesis: verum

end;

for z being set holds
( z in dom h1 iff z in dom h2 )

proof

let z be set ; :: thesis: ( z in dom h1 iff z in dom h2 )
( z in dom h1 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) by A26;
hence ( z in dom h1 iff z in dom h2 ) by A28; :: thesis: verum

end;

then dom h1 = dom h2 by TARSKI:2;
hence h1 = h2 by A30, FUNCT_1:9; :: thesis: verum