let x, x9, y, y9 be object ; :: thesis: 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; :: thesis: ( [[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 ) ) :: thesis: ( [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:| ; :: thesis: ( [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; :: thesis: verum

end;

thus ( [x,y] in dom f & [x9,y9] in dom g implies [[x,x9],[y,y9]] in dom |:f,g:| ) by Def3; :: thesis: verum