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 that
A1: D c= dom f and
A2: D c= dom g ; :: thesis: ( f | D = g | D iff for x being set st x in D holds
f . x = g . x )
A3: dom (g | D) = (dom g) /\ D by RELAT_1:61
.= D by A2, XBOOLE_1:28 ;
hereby :: thesis: ( ( for x being set st x in D holds
f . x = g . x ) implies f | D = g | D )
assume A4: 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 A5: x in D ; :: thesis: f . x = g . x
hence f . x = (g | D) . x by A4, Th48
.= g . x by A5, Th48 ;
:: thesis: verum
end;
end;
assume A6: for x being set st x in D holds
f . x = g . x ; :: thesis: f | D = g | D
A7: now :: thesis: for x being object st x in D holds
(f | D) . x = (g | D) . x
let x be object ; :: thesis: ( x in D implies (f | D) . x = (g | D) . x )
assume A8: x in D ; :: thesis: (f | D) . x = (g | D) . x
hence (f | D) . x = f . x by Th48
.= g . x by A6, A8
.= (g | D) . x by A8, Th48 ;
:: thesis: verum
end;
dom (f | D) = (dom f) /\ D by RELAT_1:61
.= D by A1, XBOOLE_1:28 ;
hence f | D = g | D by A3, A7; :: thesis: verum