let f, g be Function; :: thesis: for D being set st D c= dom f & D c= dom g holds
( f | D = g | D iff for x being set st x in D holds
f . x = g . x )
let D be set ; :: thesis: ( D c= dom f & D c= dom g implies ( f | D = g | D iff for x being set st x in D holds
f . x = g . x ) )
assume A1: ( D c= dom f & D c= dom g ) ; :: thesis: ( f | D = g | D iff for x being set st x in D holds
f . x = g . x )

hereby :: thesis: ( ( for x being set st x in D holds
f . x = g . x ) implies f | D = g | D )

assume A2: f | D = g | D ; :: thesis: for x being set st x in D holds
f . x = g . x

hereby :: thesis: verum

let x be set ; :: thesis: ( x in D implies f . x = g . x )
assume A3: x in D ; :: thesis: f . x = g . x
hence f . x = (g | D) . x by A2, Th72
.= g . x by A3, Th72 ;
:: thesis: verum

end;

end;

assume A4: for x being set st x in D holds
f . x = g . x ; :: thesis: f | D = g | D
A5: dom (f | D) = (dom f) /\ D by RELAT_1:90
.= D by A1, XBOOLE_1:28 ;
A6: dom (g | D) = (dom g) /\ D by RELAT_1:90
.= D by A1, XBOOLE_1:28 ;

now

let x be set ; :: thesis: ( x in D implies (f | D) . x = (g | D) . x )
assume A7: x in D ; :: thesis: (f | D) . x = (g | D) . x
hence (f | D) . x = f . x by Th72
.= g . x by A4, A7
.= (g | D) . x by A7, Th72 ;
:: thesis: verum

end;

hence f | D = g | D by A5, A6, Th9; :: thesis: verum