scheme :: MODELC_1:sch 1
ExistPath{ F₁() -> non empty set , F₂() -> total Relation of F₁(),F₁(), F₃() -> Element of F₁(), F₄( Element of F₁()) -> set } :

ex f being sequence of F₁() st
( f . 0 = F₃() & ( for n being Element of NAT holds
( [(f . n),(f . (n + 1))] in F₂() & f . (n + 1) in F₄((f . n)) ) ) )

provided

A1: for s being Element of F₁() holds (Im (F₂(),s)) /\ F₄(s) is non empty Subset of F₁()