:: deftheorem Def3 defines |: FUNCT_4:def 3 :
for f, g, b₃ being Function holds
( b₃ = |:f,g:| iff ( ( for z being object holds
( z in dom b₃ 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
b₃ . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) ) );