:: deftheorem Def1 defines .\/ LEXBFS:def 2 :
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 f) \/ (dom g) holds
b₃ . x = (f . x) \/ (g . x) ) ) );