:: deftheorem Def69 defines PathConc MODELC_1:def 69 :
for S being non empty set
for R being total Relation of S,S
for pai1, pai2 being inf_path of R
for k being Nat
for b₆ being sequence of S holds
( b₆ = PathConc (pai1,pai2,k) iff for n being Nat holds b₆ . n = PathChange (pai1,pai2,k,n) );