let p, q be Function; :: thesis: for A being set st dom p c= A & dom q misses A holds
(p +* q) | A = p
let A be set ; :: thesis: ( dom p c= A & dom q misses A implies (p +* q) | A = p )
assume that
A1: dom p c= A and
A2: dom q misses A ; :: thesis: (p +* q) | A = p
thus (p +* q) | A = p | A by A2, Th72
.= p by A1, RELAT_1:68 ; :: thesis: verum