:: deftheorem Def61 defines PrePath MODELC_1:def 61 :
for S being non empty set
for R being total Relation of S,S
for s0 being Element of S
for pai being inf_path of R
for n being object holds
( ( n = 0 implies PrePath (n,s0,pai) = s0 ) & ( not n = 0 implies PrePath (n,s0,pai) = pai . (k_nat ((k_nat n) - 1)) ) );