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
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
; for n being Nat holds IT . n = PathChange (pai1,pai2,k,n)
let n be Nat; 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; verum