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

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