:: deftheorem Def68 defines PathChange MODELC_1:def 68 :
for S being non empty set
for R being total Relation of S,S
for pai1, pai2 being inf_path of R
for n, k being Nat holds
( ( n < k implies PathChange (pai1,pai2,k,n) = pai1 . n ) & ( not n < k implies PathChange (pai1,pai2,k,n) = pai2 . (n - k) ) );