let f, g, h be Function; :: thesis: ( f +* h = g +* h iff f,g equal_outside dom h )
thus ( f +* h = g +* h implies f,g equal_outside dom h ) :: thesis: ( f,g equal_outside dom h implies f +* h = g +* h )

proof

assume A1: f +* h = g +* h ; :: thesis: f,g equal_outside dom h
A2: f,f +* h equal_outside dom h by Th31;
f +* h,g equal_outside dom h by A1, Th28, Th31;
hence f,g equal_outside dom h by A2, Th29; :: thesis: verum

end;

assume A3: f,g equal_outside dom h ; :: thesis: f +* h = g +* h
then A4: (dom f) \ (dom h) = (dom g) \ (dom h) by Th30;
A5: dom (f +* h) = (dom f) \/ (dom h) by FUNCT_4:def 1
.= ((dom g) \ (dom h)) \/ (dom h) by A4, XBOOLE_1:39
.= (dom g) \/ (dom h) by XBOOLE_1:39
.= dom (g +* h) by FUNCT_4:def 1 ;
for x being set st x in dom (f +* h) holds
(f +* h) . x = (g +* h) . x

proof

let x be set ; :: thesis: ( x in dom (f +* h) implies (f +* h) . x = (g +* h) . x )
assume A6: x in dom (f +* h) ; :: thesis: (f +* h) . x = (g +* h) . x

per cases ( x in dom h or not x in dom h ) ;

suppose A7: x in dom h ; :: thesis: (f +* h) . x = (g +* h) . x

hence (f +* h) . x = h . x by FUNCT_4:14
.= (g +* h) . x by A7, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A8: not x in dom h ; :: thesis: (f +* h) . x = (g +* h) . x

A9: f | ((dom f) \ (dom h)) = g | ((dom g) \ (dom h)) by A3, Def2;
dom (f +* h) = (dom f) \/ (dom h) by FUNCT_4:def 1;
then x in dom f by A6, A8, XBOOLE_0:def 3;
then A10: x in (dom f) \ (dom h) by A8, XBOOLE_0:def 5;
thus (f +* h) . x = f . x by A8, FUNCT_4:12
.= (g | ((dom g) \ (dom h))) . x by A9, A10, FUNCT_1:72
.= g . x by A4, A10, FUNCT_1:72
.= (g +* h) . x by A8, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

hence f +* h = g +* h by A5, FUNCT_1:9; :: thesis: verum