let x, y be set ; :: thesis: for E being non empty set
for u, v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
let E be non empty set ; :: thesis: for u, v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
let u, v, w be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; :: thesis: for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
let p be RedSequence of ==>.-relation TS; :: thesis: ( p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] implies ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] ) )
assume that
A1: p . 1 = [x,(u ^ w)] and
A2: p . (len p) = [y,(v ^ w)] ; :: thesis: ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
A3: len p >= 0 + 1 by NAT_1:13;
then 1 in dom p by FINSEQ_3:25;
then A4: dim2 ((p . 1),E) = (p . 1) `2 by A1, REWRITE3:51
.= u ^ w by A1 ;
deffunc H<sub>1</sub>( set ) -> object = [((p . $1) `1),(chop ((dim2 ((p . $1),E)),w))];
consider q being FinSequence such that
A5: len q = len p and
A6: for k being Nat st k in dom q holds
q . k = H₁(k) from FINSEQ_1:sch 2();
A7: for k being Nat st k in dom q & k + 1 in dom q holds
[(q . k),(q . (k + 1))] in ==>.-relation TS

proof

let k be Nat; :: thesis: ( k in dom q & k + 1 in dom q implies [(q . k),(q . (k + 1))] in ==>.-relation TS )
assume that
A8: k in dom q and
A9: k + 1 in dom q ; :: thesis: [(q . k),(q . (k + 1))] in ==>.-relation TS
( 1 <= k & k <= len q ) by A8, FINSEQ_3:25;
then A10: k in dom p by A5, FINSEQ_3:25;
then consider v1 being Element of E ^omega such that
A11: (p . k) `2 = v1 ^ (v ^ w) by A2, REWRITE3:52;
( 1 <= k + 1 & k + 1 <= len q ) by A9, FINSEQ_3:25;
then A12: k + 1 in dom p by A5, FINSEQ_3:25;
then consider v2 being Element of E ^omega such that
A13: (p . (k + 1)) `2 = v2 ^ (v ^ w) by A2, REWRITE3:52;
A14: [(p . k),(p . (k + 1))] in ==>.-relation TS by A10, A12, REWRITE1:def 2;
then [(p . k),[((p . (k + 1)) `1),(v2 ^ (v ^ w))]] in ==>.-relation TS by A10, A12, A13, REWRITE3:48;
then [[((p . k) `1),(v1 ^ (v ^ w))],[((p . (k + 1)) `1),(v2 ^ (v ^ w))]] in ==>.-relation TS by A10, A12, A11, REWRITE3:48;
then (p . k) `1 ,v1 ^ (v ^ w) ==>. (p . (k + 1)) `1 ,v2 ^ (v ^ w),TS by REWRITE3:def 4;
then consider u1 being Element of E ^omega such that
A15: (p . k) `1 ,u1 -->. (p . (k + 1)) `1 ,TS and
A16: v1 ^ (v ^ w) = u1 ^ (v2 ^ (v ^ w)) by REWRITE3:22;
A17: ex r1 being Element of TS ex w1 being Element of E ^omega ex r2 being Element of TS ex w2 being Element of E ^omega st
( p . k = [r1,w1] & p . (k + 1) = [r2,w2] ) by A14, REWRITE3:31;
then dim2 ((p . (k + 1)),E) = v2 ^ (v ^ w) by A13, REWRITE3:def 5;
then A18: q . (k + 1) = [((p . (k + 1)) `1),(chop ((v2 ^ (v ^ w)),w))] by A6, A9
.= [((p . (k + 1)) `1),(chop (((v2 ^ v) ^ w),w))] by AFINSQ_1:27
.= [((p . (k + 1)) `1),(v2 ^ v)] by Def9 ;
(v1 ^ v) ^ w = u1 ^ (v2 ^ (v ^ w)) by A16, AFINSQ_1:27
.= (u1 ^ v2) ^ (v ^ w) by AFINSQ_1:27
.= ((u1 ^ v2) ^ v) ^ w by AFINSQ_1:27 ;
then v1 ^ v = (u1 ^ v2) ^ v by AFINSQ_1:28
.= u1 ^ (v2 ^ v) by AFINSQ_1:27 ;
then A19: (p . k) `1 ,v1 ^ v ==>. (p . (k + 1)) `1 ,v2 ^ v,TS by A15, REWRITE3:def 3;
dim2 ((p . k),E) = v1 ^ (v ^ w) by A11, A17, REWRITE3:def 5;
then q . k = [((p . k) `1),(chop ((v1 ^ (v ^ w)),w))] by A6, A8
.= [((p . k) `1),(chop (((v1 ^ v) ^ w),w))] by AFINSQ_1:27
.= [((p . k) `1),(v1 ^ v)] by Def9 ;
hence [(q . k),(q . (k + 1))] in ==>.-relation TS by A19, A18, REWRITE3:def 4; :: thesis: verum

end;

len p in dom p by A3, FINSEQ_3:25;
then A20: dim2 ((p . (len p)),E) = (p . (len p)) `2 by A1, REWRITE3:51
.= v ^ w by A2 ;
reconsider q = q as RedSequence of ==>.-relation TS by A5, A7, REWRITE1:def 2;
1 in dom q by A5, A3, FINSEQ_3:25;
then A21: q . 1 = [((p . 1) `1),(chop ((dim2 ((p . 1),E)),w))] by A6
.= [x,(chop ((u ^ w),w))] by A1, A4
.= [x,u] by Def9 ;
len p in dom q by A5, A3, FINSEQ_3:25;
then q . (len q) = [((p . (len p)) `1),(chop ((dim2 ((p . (len p)),E)),w))] by A5, A6
.= [y,(chop ((v ^ w),w))] by A2, A20
.= [y,v] by Def9 ;
hence ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] ) by A21; :: thesis: verum