let f, g be non-empty Function; :: thesis: ( f tolerates g implies for x being Element of product (f +* g) holds x | (dom f) in product f )
assume A1: f tolerates g ; :: thesis: for x being Element of product (f +* g) holds x | (dom f) in product f
let x be Element of product (f +* g); :: thesis: x | (dom f) in product f
A2: ( dom x = dom (f +* g) & dom (f +* g) = (dom f) \/ (dom g) ) by CARD_3:18, FUNCT_4:def 1;
then A3: dom f c= dom x by XBOOLE_1:7;
A4: dom (x | (dom f)) = dom f by A2, RELAT_1:91, XBOOLE_1:7;

now

let z be set ; :: thesis: ( z in dom (x | (dom f)) implies (x | (dom f)) . z in f . z )
assume z in dom (x | (dom f)) ; :: thesis: (x | (dom f)) . z in f . z
then ( (x | (dom f)) . z = x . z & z in dom (f +* g) & (f +* g) . z = f . z ) by A1, A2, A3, A4, FUNCT_1:70, FUNCT_4:16;
hence (x | (dom f)) . z in f . z by CARD_3:18; :: thesis: verum

end;

hence x | (dom f) in product f by A4, CARD_3:18; :: thesis: verum