let R be Relation; 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; 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; ( 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
; ( q1 is RedSequence of R & q2 is RedSequence of R )
now for i being Nat st i in dom q1 & i + 1 in dom q1 holds
[(q1 . i),(q1 . (i + 1))] in Rlet i be
Nat;
( 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
;
[(q1 . i),(q1 . (i + 1))] in RA6:
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;
verum end;
hence
q1 is RedSequence of R
by A2, REWRITE1:def 2; q2 is RedSequence of R
now for i being Nat st i in dom q2 & i + 1 in dom q2 holds
[(q2 . i),(q2 . (i + 1))] in Rlet i be
Nat;
( 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
;
[(q2 . i),(q2 . (i + 1))] in RA16:
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;
verum end;
hence
q2 is RedSequence of R
by A3, REWRITE1:def 2; verum