let f1, f2 be sequence of S; ( ( for n being Nat holds f1 . n = PathChange (pai1,pai2,k,n) ) & ( for n being Nat holds f2 . n = PathChange (pai1,pai2,k,n) ) implies f1 = f2 )
assume that
A5:
for n being Nat holds f1 . n = PathChange (pai1,pai2,k,n)
and
A6:
for n being Nat holds f2 . n = PathChange (pai1,pai2,k,n)
; f1 = f2
for x being object st x in NAT holds
f1 . x = f2 . x
hence
f1 = f2
by FUNCT_2:12; verum