let V, A be set ; :: thesis: for f, g being finite Function st f tolerates g & f in NDSS (V,A) & g in NDSS (V,A) holds
f \/ g in NDSS (V,A)
let f, g be finite Function; :: thesis: ( f tolerates g & f in NDSS (V,A) & g in NDSS (V,A) implies f \/ g in NDSS (V,A) )
assume A1: f tolerates g ; :: thesis: ( not f in NDSS (V,A) or not g in NDSS (V,A) or f \/ g in NDSS (V,A) )
assume ( f in NDSS (V,A) & g in NDSS (V,A) ) ; :: thesis: f \/ g in NDSS (V,A)
then ( f is NominativeSet of V,A & g is NominativeSet of V,A ) by Th4;
then ( f \/ g is V -defined & f \/ g is A -valued ) ;
then f \/ g is PartFunc of V,A by A1, RELSET_1:4, PARTFUN1:51;
hence f \/ g in NDSS (V,A) ; :: thesis: verum