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 Th9;
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:62, XBOOLE_1:7;

now :: thesis: for z being object st z in dom (x | (dom f)) holds
(x | (dom f)) . z in f . z

let z be object ; :: 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:47;
(f +* g) . z = f . z by A1, A5, A6, FUNCT_4:15;
hence (x | (dom f)) . z in f . z by A2, A4, A5, A6, A7, Th9; :: thesis: verum

end;

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