let R be Relation; :: thesis: for P being RedSequence of R
for q1, q2 being FinSequence st P = q1 ^ q2 & len q1 > 0 & len q2 > 0 holds
( q1 is RedSequence of R & q2 is RedSequence of R )
let P be RedSequence of R; :: thesis: for q1, q2 being FinSequence st P = q1 ^ q2 & len q1 > 0 & len q2 > 0 holds
( q1 is RedSequence of R & q2 is RedSequence of R )
let q1, q2 be FinSequence; :: thesis: ( P = q1 ^ q2 & len q1 > 0 & len q2 > 0 implies ( q1 is RedSequence of R & q2 is RedSequence of R ) )
assume that
A1: P = q1 ^ q2 and
A2: len q1 > 0 and
A3: len q2 > 0 ; :: thesis: ( q1 is RedSequence of R & q2 is RedSequence of R )

now :: thesis: for i being Nat st i in dom q1 & i + 1 in dom q1 holds
[(q1 . i),(q1 . (i + 1))] in R

let i be Nat; :: thesis: ( i in dom q1 & i + 1 in dom q1 implies [(q1 . i),(q1 . (i + 1))] in R )
assume that
A4: i in dom q1 and
A5: i + 1 in dom q1 ; :: thesis: [(q1 . i),(q1 . (i + 1))] in R
A6: i + 1 <= len q1 by A5, FINSEQ_3:25;
A7: 1 <= i + 1 by A5, FINSEQ_3:25;
then A8: q1 . (i + 1) = (q1 ^ q2) . (i + 1) by A6, FINSEQ_1:64;
A9: len q1 <= len P by A1, CALCUL_1:6;
then i + 1 <= len P by A6, XXREAL_0:2;
then A10: i + 1 in dom P by A7, FINSEQ_3:25;
A11: 1 <= i by A4, FINSEQ_3:25;
A12: i <= len q1 by A4, FINSEQ_3:25;
then i <= len P by A9, XXREAL_0:2;
then A13: i in dom P by A11, FINSEQ_3:25;
q1 . i = (q1 ^ q2) . i by A11, A12, FINSEQ_1:64;
hence [(q1 . i),(q1 . (i + 1))] in R by A1, A8, A13, A10, REWRITE1:def 2; :: thesis: verum

end;

hence q1 is RedSequence of R by A2, REWRITE1:def 2; :: thesis: q2 is RedSequence of R

now :: thesis: for i being Nat st i in dom q2 & i + 1 in dom q2 holds
[(q2 . i),(q2 . (i + 1))] in R

let i be Nat; :: thesis: ( i in dom q2 & i + 1 in dom q2 implies [(q2 . i),(q2 . (i + 1))] in R )
assume that
A14: i in dom q2 and
A15: i + 1 in dom q2 ; :: thesis: [(q2 . i),(q2 . (i + 1))] in R
A16: 1 <= i + 1 by A15, FINSEQ_3:25;
then A17: 1 <= (i + 1) + (len q1) by NAT_1:12;
A18: 1 <= i by A14, FINSEQ_3:25;
then A19: 1 <= i + (len q1) by NAT_1:12;
A20: i + 1 <= len q2 by A15, FINSEQ_3:25;
then A21: q2 . (i + 1) = (q1 ^ q2) . ((len q1) + (i + 1)) by A16, FINSEQ_1:65;
A22: (len q1) + (len q2) = len P by A1, FINSEQ_1:22;
then (len q1) + (i + 1) <= ((len P) - (len q2)) + (len q2) by A20, XREAL_1:7;
then A23: ((len q1) + i) + 1 in dom P by A17, FINSEQ_3:25;
A24: i <= len q2 by A14, FINSEQ_3:25;
then (len q1) + i <= ((len P) - (len q2)) + (len q2) by A22, XREAL_1:7;
then A25: (len q1) + i in dom P by A19, FINSEQ_3:25;
q2 . i = (q1 ^ q2) . ((len q1) + i) by A18, A24, FINSEQ_1:65;
hence [(q2 . i),(q2 . (i + 1))] in R by A1, A21, A25, A23, REWRITE1:def 2; :: thesis: verum

end;

hence q2 is RedSequence of R by A3, REWRITE1:def 2; :: thesis: verum