deffunc H1( object ) -> set = PathChange (pai1,pai2,k,(k_nat $1));
A1: for n being object st n in NAT holds
H1(n) in S
proof
let n be object ; :: thesis: ( n in NAT implies H1(n) in S )
assume n in NAT ; :: thesis: H1(n) in S
then reconsider n = n as Element of NAT ;
set x = PathChange (pai1,pai2,k,n);
A2: H1(n) = PathChange (pai1,pai2,k,n) by Def2;
per cases ( n < k or not n < k ) ;
suppose n < k ; :: thesis: H1(n) in S
then PathChange (pai1,pai2,k,n) = pai1 . n by Def68;
hence H1(n) in S by A2; :: thesis: verum
end;
suppose A3: not n < k ; :: thesis: H1(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 H1(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 = H1(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