let x, x9, y, y9 be object ; for f, g being Function holds
( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) )
let f, g be Function; ( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) )
thus
( [[x,x9],[y,y9]] in dom |:f,g:| implies ( [x,y] in dom f & [x9,y9] in dom g ) )
( [x,y] in dom f & [x9,y9] in dom g implies [[x,x9],[y,y9]] in dom |:f,g:| )proof
assume
[[x,x9],[y,y9]] in dom |:f,g:|
;
( [x,y] in dom f & [x9,y9] in dom g )
then consider x1,
y1,
x19,
y19 being
object such that A1:
[[x,x9],[y,y9]] = [[x1,x19],[y1,y19]]
and A2:
(
[x1,y1] in dom f &
[x19,y19] in dom g )
by Def3;
(
x = x1 &
x9 = x19 )
by A1, Lm1;
hence
(
[x,y] in dom f &
[x9,y9] in dom g )
by A1, A2, Lm1;
verum
end;
thus
( [x,y] in dom f & [x9,y9] in dom g implies [[x,x9],[y,y9]] in dom |:f,g:| )
by Def3; verum