let f be Function; :: thesis: for g, h being one-to-one Function st h = f +* g holds
(h ") | (rng g) = g "
let g, h be one-to-one Function; :: thesis: ( h = f +* g implies (h ") | (rng g) = g " )
assume A1: h = f +* g ; :: thesis: (h ") | (rng g) = g "
A2: dom ((h ") | (rng g)) = (dom (h ")) /\ (rng g) by RELAT_1:61
.= (rng h) /\ (rng g) by FUNCT_1:33
.= ((f .: ((dom f) \ (dom g))) \/ (rng g)) /\ (rng g) by A1, FRECHET:12
.= rng g by XBOOLE_1:21
.= dom (g ") by FUNCT_1:33 ;

now :: thesis: for y being object st y in dom (g ") holds
(g ") . y = ((h ") | (rng g)) . y

let y be object ; :: thesis: ( y in dom (g ") implies (g ") . y = ((h ") | (rng g)) . y )
assume y in dom (g ") ; :: thesis: (g ") . y = ((h ") | (rng g)) . y
then A3: y in rng g by FUNCT_1:33;
then consider x being object such that
A4: ( x in dom g & g . x = y ) by FUNCT_1:def 3;
dom h = (dom f) \/ (dom g) by A1, FUNCT_4:def 1;
then A5: x in dom h by A4, XBOOLE_0:def 3;
thus (g ") . y = x by A4, FUNCT_1:34
.= (h ") . (h . x) by A5, FUNCT_1:34
.= (h ") . y by A1, A4, FUNCT_4:13
.= ((h ") | (rng g)) . y by A3, FUNCT_1:49 ; :: thesis: verum

end;

hence (h ") | (rng g) = g " by A2, FUNCT_1:2; :: thesis: verum