let f, g, h be Function; :: thesis: for D being set st (f +* g) | D = h | D holds
(h +* g) | D = (f +* g) | D
let D be set ; :: thesis: ( (f +* g) | D = h | D implies (h +* g) | D = (f +* g) | D )
assume A1: (f +* g) | D = h | D ; :: thesis: (h +* g) | D = (f +* g) | D
A2: dom ((f +* g) | D) = (dom (f +* g)) /\ D by RELAT_1:61
.= ((dom f) \/ (dom g)) /\ D by Def1 ;
A3: dom ((h +* g) | D) = (dom (h +* g)) /\ D by RELAT_1:61
.= ((dom h) \/ (dom g)) /\ D by Def1 ;
then A4: dom ((h +* g) | D) = ((dom h) /\ D) \/ ((dom g) /\ D) by XBOOLE_1:23
.= (((dom f) \/ (dom g)) /\ D) \/ ((dom g) /\ D) by A1, A2, RELAT_1:61
.= (((dom f) \/ (dom g)) \/ (dom g)) /\ D by XBOOLE_1:23
.= ((dom f) \/ ((dom g) \/ (dom g))) /\ D by XBOOLE_1:4
.= ((dom f) \/ (dom g)) /\ D ;
now :: thesis: for x being object st x in dom ((f +* g) | D) holds
((h +* g) | D) . x = ((f +* g) | D) . x
let x be object ; :: thesis: ( x in dom ((f +* g) | D) implies ((h +* g) | D) . b1 = ((f +* g) | D) . b1 )
assume A5: x in dom ((f +* g) | D) ; :: thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1
then A6: x in (dom f) \/ (dom g) by A2, XBOOLE_0:def 4;
A7: x in D by A2, A5, XBOOLE_0:def 4;
A8: ( x in (dom h) \/ (dom g) & ((h +* g) | D) . x = (h +* g) . x ) by A2, A3, A4, A5, FUNCT_1:47, XBOOLE_0:def 4;
per cases ( x in dom g or not x in dom g ) ;
suppose A9: x in dom g ; :: thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1
((f +* g) | D) . x = (f +* g) . x by A5, FUNCT_1:47
.= g . x by A6, A9, Def1 ;
hence ((h +* g) | D) . x = ((f +* g) | D) . x by A8, A9, Def1; :: thesis: verum
end;
suppose not x in dom g ; :: thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1
hence ((h +* g) | D) . x = h . x by A8, Def1
.= ((f +* g) | D) . x by A1, A7, FUNCT_1:49 ;
:: thesis: verum
end;
end;
end;
hence (h +* g) | D = (f +* g) | D by A2, A4; :: thesis: verum