let f be Function; :: thesis: for A, B being set st dom f c= A \/ B holds
(f | A) +* (f | B) = f
let A, B be set ; :: thesis: ( dom f c= A \/ B implies (f | A) +* (f | B) = f )
A1: ( dom (f | A) = (dom f) /\ A & dom (f | B) = (dom f) /\ B ) by RELAT_1:61;
A2: for x being object st x in (dom (f | A)) \/ (dom (f | B)) holds
( ( x in dom (f | B) implies f . x = (f | B) . x ) & ( not x in dom (f | B) implies f . x = (f | A) . x ) )

proof

let x be object ; :: thesis: ( x in (dom (f | A)) \/ (dom (f | B)) implies ( ( x in dom (f | B) implies f . x = (f | B) . x ) & ( not x in dom (f | B) implies f . x = (f | A) . x ) ) )
assume A3: x in (dom (f | A)) \/ (dom (f | B)) ; :: thesis: ( ( x in dom (f | B) implies f . x = (f | B) . x ) & ( not x in dom (f | B) implies f . x = (f | A) . x ) )
thus ( x in dom (f | B) implies f . x = (f | B) . x ) by FUNCT_1:47; :: thesis: ( not x in dom (f | B) implies f . x = (f | A) . x )
assume not x in dom (f | B) ; :: thesis: f . x = (f | A) . x
then x in dom (f | A) by A3, XBOOLE_0:def 3;
hence f . x = (f | A) . x by FUNCT_1:47; :: thesis: verum

end;

assume dom f c= A \/ B ; :: thesis: (f | A) +* (f | B) = f
then dom f = (dom f) /\ (A \/ B) by XBOOLE_1:28
.= (dom (f | A)) \/ (dom (f | B)) by A1, XBOOLE_1:23 ;
hence (f | A) +* (f | B) = f by A2, Def1; :: thesis: verum