let x, x', y, y' be set ; :: thesis: for f, g being Function holds
( [[x,x'],[y,y']] in dom |:f,g:| iff ( [x,y] in dom f & [x',y'] in dom g ) )
let f, g be Function; :: thesis: ( [[x,x'],[y,y']] in dom |:f,g:| iff ( [x,y] in dom f & [x',y'] in dom g ) )
thus ( [[x,x'],[y,y']] in dom |:f,g:| implies ( [x,y] in dom f & [x',y'] in dom g ) ) :: thesis: ( [x,y] in dom f & [x',y'] in dom g implies [[x,x'],[y,y']] in dom |:f,g:| )

proof

assume [[x,x'],[y,y']] in dom |:f,g:| ; :: thesis: ( [x,y] in dom f & [x',y'] in dom g )
then consider x1, y1, x1', y1' being set such that
A1: [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']] and
A2: ( [x1,y1] in dom f & [x1',y1'] in dom g ) by Def3;
( x = x1 & y = y1 & x' = x1' & y' = y1' ) by A1, Lm2;
hence ( [x,y] in dom f & [x',y'] in dom g ) by A2; :: thesis: verum

end;

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