:: deftheorem Def2 defines Intersect YELLOW20:def 2 :
for f, g, b₃ being Function holds
( b₃ = Intersect (f,g) iff ( dom b₃ = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds
b₃ . x = (f . x) /\ (g . x) ) ) );