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

proof

let n be object ; :: 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 sequence of S such that
A4: for n being object st n in NAT holds
IT . n = H₁(n) from FUNCT_2:sch 2(A1);
take IT ; :: thesis: for n being Nat holds IT . n = PathChange (pai1,pai2,k,n)
let n be Nat; :: thesis: IT . n = PathChange (pai1,pai2,k,n)
n in NAT by ORDINAL1:def 12;
then k_nat n = n by Def2;
hence IT . n = PathChange (pai1,pai2,k,n) by A4; :: thesis: verum