scheme :: REWRITE1:sch 1
PathCatenation{ P1[ set , set ], F1() -> FinSequence, F2() -> FinSequence } :
for i being Nat st i in dom (F1() $^ F2()) & i + 1 in dom (F1() $^ F2()) holds
for x, y being set st x = (F1() $^ F2()) . i & y = (F1() $^ F2()) . (i + 1) holds
P1[x,y]
provided
A1: for i being Nat st i in dom F1() & i + 1 in dom F1() holds
P1[F1() . i,F1() . (i + 1)] and
A2: for i being Nat st i in dom F2() & i + 1 in dom F2() holds
P1[F2() . i,F2() . (i + 1)] and
A3: ( len F1() > 0 & len F2() > 0 & F1() . (len F1()) = F2() . 1 )