let R be Relation; for p, q being RedSequence of R st p . (len p) = q . 1 holds
p $^ q is RedSequence of R
let p, q be RedSequence of R; ( p . (len p) = q . 1 implies p $^ q is RedSequence of R )
defpred S1[ set , set ] means [$1,$2] in R;
set r = p $^ q;
consider p1 being FinSequence, x being object such that
A1:
p = p1 ^ <*x*>
by FINSEQ_1:46;
assume
p . (len p) = q . 1
; p $^ q is RedSequence of R
then A2:
( len p > 0 & len q > 0 & p . (len p) = q . 1 )
;
p $^ q = p1 ^ q
by A1, Th2;
hence
len (p $^ q) > 0
; REWRITE1:def 2 for i being Nat st i in dom (p $^ q) & i + 1 in dom (p $^ q) holds
[((p $^ q) . i),((p $^ q) . (i + 1))] in R
A3:
for i being Nat st i in dom q & i + 1 in dom q holds
S1[q . i,q . (i + 1)]
by Def2;
A4:
for i being Nat st i in dom p & i + 1 in dom p holds
S1[p . i,p . (i + 1)]
by Def2;
for i being Nat st i in dom (p $^ q) & i + 1 in dom (p $^ q) holds
for x, y being set st x = (p $^ q) . i & y = (p $^ q) . (i + 1) holds
S1[x,y]
from REWRITE1:sch 1(A4, A3, A2);
hence
for i being Nat st i in dom (p $^ q) & i + 1 in dom (p $^ q) holds
[((p $^ q) . i),((p $^ q) . (i + 1))] in R
; verum