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 f +* h = g +* h ; :: thesis: f,g equal_outside dom h
then A1: f +* h,g equal_outside dom h by Th25, Th28;
f,f +* h equal_outside dom h by Th28;
hence f,g equal_outside dom h by A1; :: thesis: verum

end;

assume A2: f,g equal_outside dom h ; :: thesis: f +* h = g +* h
then A3: (dom f) \ (dom h) = (dom g) \ (dom h) by Th27;
A4: for x being object st x in dom (f +* h) holds
(f +* h) . x = (g +* h) . x

proof

let x be object ; :: thesis: ( x in dom (f +* h) implies (f +* h) . x = (g +* h) . x )
assume A5: 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 A6: x in dom h ; :: thesis: (f +* h) . x = (g +* h) . x

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

end;

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

dom (f +* h) = (dom f) \/ (dom h) by FUNCT_4:def 1;
then x in dom f by A5, A7, XBOOLE_0:def 3;
then A8: x in (dom f) \ (dom h) by A7, XBOOLE_0:def 5;
A9: f | ((dom f) \ (dom h)) = g | ((dom g) \ (dom h)) by A2;
thus (f +* h) . x = f . x by A7, FUNCT_4:11
.= (g | ((dom g) \ (dom h))) . x by A9, A8, FUNCT_1:49
.= g . x by A3, A8, FUNCT_1:49
.= (g +* h) . x by A7, FUNCT_4:11 ; :: thesis: verum

end;

end;

end;

dom (f +* h) = (dom f) \/ (dom h) by FUNCT_4:def 1
.= ((dom g) \ (dom h)) \/ (dom h) by A3, XBOOLE_1:39
.= (dom g) \/ (dom h) by XBOOLE_1:39
.= dom (g +* h) by FUNCT_4:def 1 ;
hence f +* h = g +* h by A4; :: thesis: verum