:: deftheorem Def8 defines [: FUNCT_3:def 8 :
for f, g, b₃ being Function holds
( b₃ = [:f,g:] iff ( dom b₃ = [:(dom f),(dom g):] & ( for x, y being object st x in dom f & y in dom g holds
b₃ . (x,y) = [(f . x),(g . y)] ) ) );