let f, g be Function; :: thesis: for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {x,y,z} = g | {x,y,z}
let x, y, z be set ; :: thesis: ( dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z implies f | {x,y,z} = g | {x,y,z} )
assume that
A1: dom f = dom g and
A2: ( f . x = g . x & f . y = g . y ) and
A3: f . z = g . z ; :: thesis: f | {x,y,z} = g | {x,y,z}
A4: f | {x,y} = g | {x,y} by A1, A2, Th91;
A5: f | {z} = g | {z} by A1, A3, Th90;
{x,y,z} = {x,y} \/ {z} by ENUMSET1:43;
hence f | {x,y,z} = g | {x,y,z} by A4, A5, RELAT_1:185; :: thesis: verum