let f, g be Function; :: thesis: for A being set st A /\ (dom f) c= A /\ (dom g) holds
(f +* (g | A)) | A = g | A
let A be set ; :: thesis: ( A /\ (dom f) c= A /\ (dom g) implies (f +* (g | A)) | A = g | A )
assume A1: A /\ (dom f) c= A /\ (dom g) ; :: thesis: (f +* (g | A)) | A = g | A
A2: ( dom (f | A) = A /\ (dom f) & dom (g | A) = A /\ (dom g) ) by RELAT_1:61;
thus (f +* (g | A)) | A = (f | A) +* ((g | A) | A) by Th71
.= (f | A) +* (g | A)
.= g | A by A1, A2, Th19 ; :: thesis: verum