defpred S₁[ object , object ] means ex c being Element of (k -chain-space p) st
( $1 = c & $2 = Boundary c );
A1: for x being object st x in k -chains p holds
ex y being object st
( y in (k - 1) -chains p & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in k -chains p implies ex y being object st
( y in (k - 1) -chains p & S₁[x,y] ) )
assume x in k -chains p ; :: thesis: ex y being object st
( y in (k - 1) -chains p & S₁[x,y] )
then reconsider x = x as Element of (k -chain-space p) ;
set b = Boundary x;
take Boundary x ; :: thesis: ( Boundary x in (k - 1) -chains p & S₁[x, Boundary x] )
thus ( Boundary x in (k - 1) -chains p & S₁[x, Boundary x] ) ; :: thesis: verum

end;

consider f being Function of (k -chains p),((k - 1) -chains p) such that
A2: for x being object st x in k -chains p holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
reconsider f = f as Function of (k -chain-space p),((k - 1) -chain-space p) ;
take f ; :: 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 f . c = Boundary c

proof

let c be Element of (k -chain-space p); :: thesis: f . c = Boundary c
S₁[c,f . c] by A2;
hence f . c = Boundary c ; :: thesis: verum

end;

hence for c being Element of (k -chain-space p) holds f . c = Boundary c ; :: thesis: verum