let h1, h2 be Function; :: thesis: ( ( for z being object holds
( z in dom h1 iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being object 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 object holds
( z in dom h2 iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being object 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 object holds
( z in dom h1 iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) and
A27: for x, y, x9, y9 being object 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 object holds
( z in dom h2 iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) and
A29: for x, y, x9, y9 being object 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 object st z in dom h1 holds
h1 . z = h2 . z
proof
let z be object ; :: 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 object 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 object holds
( z in dom h1 iff z in dom h2 )
proof
let z be object ; :: thesis: ( z in dom h1 iff z in dom h2 )
( z in dom h1 iff ex x, y, x9, y9 being object 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; :: thesis: verum