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
A3: for c being Element of (k -chain-space p) holds f . c = Boundary c and
A4: for c being Element of (k -chain-space p) holds g . c = Boundary c ; :: thesis: f = g
A5: for x being object st x in dom f holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
then reconsider x = x as Element of (k -chain-space p) ;
f . x = Boundary x by A3;
hence f . x = g . x by A4; :: thesis: verum

end;

dom f = [#] (k -chain-space p) by FUNCT_2:def 1;
then dom f = dom g by FUNCT_2:def 1;
hence f = g by A5, FUNCT_1:2; :: thesis: verum