let f, g be Function of (k -chain-space p),((k - 1) -chain-space p); :: thesis: ( ( for c being Element of (k -chain-space p) holds f . c = Boundary c ) & ( for c being Element of (k -chain-space p) holds g . c = Boundary c ) implies f = g )
assume that
A5: for c being Element of (k -chain-space p) holds f . c = Boundary c and
A6: for c being Element of (k -chain-space p) holds g . c = Boundary c ; :: thesis: f = g
dom f = [#] (k -chain-space p) by FUNCT_2:def 1;
then A7: dom f = dom g by FUNCT_2:def 1;
for x being set st x in dom f holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume A8: x in dom f ; :: thesis: f . x = g . x
reconsider x = x as Element of (k -chain-space p) by A8;
f . x = Boundary x by A5;
hence f . x = g . x by A6; :: thesis: verum

end;

hence f = g by A7, FUNCT_1:9; :: thesis: verum