deffunc H₁( set ) -> set = PathChange pai1,pai2,k,(k_nat $1);
A1: for n being set st n in NAT holds
H₁(n) in S

proof

let n be set ; :: thesis: ( n in NAT implies H₁(n) in S )
assume n in NAT ; :: thesis: H₁(n) in S
then reconsider n = n as Element of NAT ;
set x = PathChange pai1,pai2,k,n;
A2: H₁(n) = PathChange pai1,pai2,k,n by Def2;

per cases ( n < k or not n < k ) ;

suppose n < k ; :: thesis: H₁(n) in S

then PathChange pai1,pai2,k,n = pai1 . n by Def68;
hence H₁(n) in S by A2; :: thesis: verum

end;

suppose A3: not n < k ; :: thesis: H₁(n) in S

set m = n - k;
reconsider m = n - k as Element of NAT by A3, NAT_1:21;
PathChange pai1,pai2,k,n = pai2 . m by A3, Def68;
hence H₁(n) in S by A2; :: thesis: verum

end;

end;

end;

consider IT being Function of NAT ,S such that
A4: for n being set st n in NAT holds
IT . n = H₁(n) from FUNCT_2:sch 2(A1);
take IT ; :: thesis: for n being Element of NAT holds IT . n = PathChange pai1,pai2,k,n
let n be Element of NAT ; :: thesis: IT . n = PathChange pai1,pai2,k,n
k_nat n = n by Def2;
hence IT . n = PathChange pai1,pai2,k,n by A4; :: thesis: verum