let f, g be Function; :: thesis: for x being set st dom f = dom g & f . x = g . x holds
f | {x} = g | {x}
let x be set ; :: thesis: ( dom f = dom g & f . x = g . x implies f | {x} = g | {x} )
assume that
A1: dom f = dom g and
A2: f . x = g . x ; :: thesis: f | {x} = g | {x}

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

suppose A3: x in dom f ; :: thesis: f | {x} = g | {x}

hence f | {x} = {[x,(g . x)]} by A2, Th26
.= g | {x} by A1, A3, Th26 ;
:: thesis: verum

end;

suppose not x in dom f ; :: thesis: f | {x} = g | {x}

then A4: {x} misses dom f by ZFMISC_1:50;
hence f | {x} = {} by RELAT_1:66
.= g | {x} by A1, A4, RELAT_1:66 ;
:: thesis: verum

end;

end;