let h1, h2 be Function; :: thesis: ( ( for z being set holds
( z in dom h1 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h1 . [x,x9],[y,y9] = [(f . x,y),(g . x9,y9)] ) & ( for z being set holds
( z in dom h2 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h2 . [x,x9],[y,y9] = [(f . x,y),(g . x9,y9)] ) implies h1 = h2 )
assume that
A26: for z being set holds
( z in dom h1 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) and
A27: for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h1 . [x,x9],[y,y9] = [(f . x,y),(g . x9,y9)] and
A28: for z being set holds
( z in dom h2 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) and
A29: for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
h2 . [x,x9],[y,y9] = [(f . x,y),(g . x9,y9)] ; :: 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, x9, y9 being set such that
A31: z = [[x,x9],[y,y9]] and
A32: ( [x,y] in dom f & [x9,y9] in dom g ) by A26;
h1 . [x,x9],[y,y9] = [(f . x,y),(g . x9,y9)] by A27, A32
.= h2 . [x,x9],[y,y9] 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, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] 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