let x, y be set ; :: thesis: for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega )
for TS being non empty transition-system of F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
let E be non empty set ; :: thesis: for u, v, w being Element of E ^omega
for F being Subset of (E ^omega )
for TS being non empty transition-system of F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
let u, v, w be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega )
for TS being non empty transition-system of F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
let TS be non empty transition-system of F; :: thesis: ( ==>.-relation TS reduces [x,u],[y,v] implies ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] )
assume ==>.-relation TS reduces [x,u],[y,v] ; :: thesis: ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
then consider P being RedSequence of ==>.-relation TS such that
A: ( P . 1 = [x,u] & P . (len P) = [y,v] ) by REWRITE1:def 3;
deffunc H₁( set ) -> set = [((P . $1) `1 ),((dim2 (P . $1),E) ^ w)];
consider Q being FinSequence such that
B1: len Q = len P and
B2: for k being Nat st k in dom Q holds
Q . k = H₁(k) from FINSEQ_1:sch 2();
for k being Element of NAT st k in dom Q & k + 1 in dom Q holds
[(Q . k),(Q . (k + 1))] in ==>.-relation TS

proof

let k be Element of NAT ; :: thesis: ( k in dom Q & k + 1 in dom Q implies [(Q . k),(Q . (k + 1))] in ==>.-relation TS )
assume C1: ( k in dom Q & k + 1 in dom Q ) ; :: thesis: [(Q . k),(Q . (k + 1))] in ==>.-relation TS
( 1 <= k & k <= len Q & 1 <= k + 1 & k + 1 <= len Q ) by C1, FINSEQ_3:27;
then C2: ( k in dom P & k + 1 in dom P ) by B1, FINSEQ_3:27;
[(P . k),(P . (k + 1))] in ==>.-relation TS by C2, REWRITE1:def 2;
then [[((P . k) `1 ),((P . k) `2 )],(P . (k + 1))] in ==>.-relation TS by C2, ThRedSeq5;
then [[((P . k) `1 ),((P . k) `2 )],[((P . (k + 1)) `1 ),((P . (k + 1)) `2 )]] in ==>.-relation TS by C2, ThRedSeq5;
then [[((P . k) `1 ),(dim2 (P . k),E)],[((P . (k + 1)) `1 ),((P . (k + 1)) `2 )]] in ==>.-relation TS by A, C2, ThRedSeq30;
then [[((P . k) `1 ),(dim2 (P . k),E)],[((P . (k + 1)) `1 ),(dim2 (P . (k + 1)),E)]] in ==>.-relation TS by A, C2, ThRedSeq30;
then (P . k) `1 , dim2 (P . k),E ==>. (P . (k + 1)) `1 , dim2 (P . (k + 1)),E,TS by DefRel;
then (P . k) `1 ,(dim2 (P . k),E) ^ w ==>. (P . (k + 1)) `1 ,(dim2 (P . (k + 1)),E) ^ w,TS by ThDir30;
then [[((P . k) `1 ),((dim2 (P . k),E) ^ w)],[((P . (k + 1)) `1 ),((dim2 (P . (k + 1)),E) ^ w)]] in ==>.-relation TS by DefRel;
then [[((P . k) `1 ),((dim2 (P . k),E) ^ w)],(Q . (k + 1))] in ==>.-relation TS by C1, B2;
hence [(Q . k),(Q . (k + 1))] in ==>.-relation TS by C1, B2; :: thesis: verum

end;

then reconsider Q = Q as RedSequence of ==>.-relation TS by B1, REWRITE1:def 2;
D3: len P >= 0 + 1 by NAT_1:13;
then 1 in dom P by FINSEQ_3:27;
then D1: dim2 (P . 1),E = (P . 1) `2 by A, ThRedSeq30
.= u by A, MCART_1:7 ;
D0: len Q >= 0 + 1 by NAT_1:13;
then 1 in dom Q by FINSEQ_3:27;
then D: Q . 1 = [((P . 1) `1 ),((dim2 (P . 1),E) ^ w)] by B2
.= [x,(u ^ w)] by A, D1, MCART_1:7 ;
len P in dom P by D3, FINSEQ_3:27;
then D2: dim2 (P . (len P)),E = (P . (len P)) `2 by A, ThRedSeq30
.= v by A, MCART_1:7 ;
len Q in dom Q by D0, FINSEQ_3:27;
then Q . (len Q) = [((P . (len Q)) `1 ),((dim2 (P . (len Q)),E) ^ w)] by B2;
then Q . (len Q) = [y,(v ^ w)] by A, B1, D2, MCART_1:7;
hence ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] by D, REWRITE1:def 3; :: thesis: verum