let f be Function; :: thesis: for A, B being set holds f | (A \/ B) = (f | A) +* (f | B)
let A, B be set ; :: thesis: f | (A \/ B) = (f | A) +* (f | B)
A1: (f | (A \/ B)) | B = f | ((A \/ B) /\ B) by RELAT_1:71
.= f | B by XBOOLE_1:21 ;
A2: dom (f | (A \/ B)) c= A \/ B by RELAT_1:58;
(f | (A \/ B)) | A = f | ((A \/ B) /\ A) by RELAT_1:71
.= f | A by XBOOLE_1:21 ;
hence f | (A \/ B) = (f | A) +* (f | B) by A1, A2, Th70; :: thesis: verum