let R be Relation; :: thesis: 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; :: thesis: ( p . (len p) = q . 1 implies p $^ q is RedSequence of R )
defpred S₁[ 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 ; :: thesis: 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 ; :: according to REWRITE1:def 2 :: thesis: 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
S₁[q . i,q . (i + 1)] by Def2;
A4: for i being Nat st i in dom p & i + 1 in dom p holds
S₁[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
S₁[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 ; :: thesis: verum