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) by Th18;
A3: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
then A4: dom f c= dom x by A2, XBOOLE_1:7;
A5: dom (x | (dom f)) = dom f by A2, A3, 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 A6: z in dom (x | (dom f)) ; :: thesis: (x | (dom f)) . z in f . z
then A7: (x | (dom f)) . z = x . z by FUNCT_1:70;
(f +* g) . z = f . z by A1, A5, A6, FUNCT_4:16;
hence (x | (dom f)) . z in f . z by A2, A4, A5, A6, A7, Th18; :: thesis: verum

end;

hence x | (dom f) in product f by A5, Th18; :: thesis: verum