:: deftheorem Def7 defines <: FUNCT_3:def 7 :
for f, g, b₃ being Function holds
( b₃ = <:f,g:> iff ( dom b₃ = (dom f) /\ (dom g) & ( for x being object st x in dom b₃ holds
b₃ . x = [(f . x),(g . x)] ) ) );