scheme :: REWRITE1:sch 1
PathCatenation{ P₁[ set , set ], F₁() -> FinSequence, F₂() -> FinSequence } :

for i being Nat st i in dom (F₁() $^ F₂()) & i + 1 in dom (F₁() $^ F₂()) holds
for x, y being set st x = (F₁() $^ F₂()) . i & y = (F₁() $^ F₂()) . (i + 1) holds
P₁[x,y]

provided

A1: for i being Nat st i in dom F₁() & i + 1 in dom F₁() holds
P₁[F₁() . i,F₁() . (i + 1)] and
A2: for i being Nat st i in dom F₂() & i + 1 in dom F₂() holds
P₁[F₂() . i,F₂() . (i + 1)] and
A3: ( len F₁() > 0 & len F₂() > 0 & F₁() . (len F₁()) = F₂() . 1 )