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 Def70;
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, Def70;
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