let f, g be Function; :: thesis: for w, x, y, z being object st dom f = dom g & f . w = g . w & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {w,x,y,z} = g | {w,x,y,z}
let w, x, y, z be object ; :: thesis: ( dom f = dom g & f . w = g . w & f . x = g . x & f . y = g . y & f . z = g . z implies f | {w,x,y,z} = g | {w,x,y,z} )
assume ( dom f = dom g & f . w = g . w & f . x = g . x & f . y = g . y & f . z = g . z ) ; :: thesis: f | {w,x,y,z} = g | {w,x,y,z}
then A1: ( f | {w,x,y} = g | {w,x,y} & f | {z} = g | {z} ) by GRFUNC_1:29, GRFUNC_1:31;
{w,x,y,z} = {w,x,y} \/ {z} by ENUMSET1:6;
hence f | {w,x,y,z} = g | {w,x,y,z} by A1, RELAT_1:150; :: thesis: verum