let x, y be object ; :: 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 over 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 over 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 over 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 over 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 over 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
A1: P . 1 = [x,u] and
A2: P . (len P) = [y,v] by REWRITE1:def 3;
A3: len P >= 0 + 1 by NAT_1:13;
then len P in dom P by FINSEQ_3:25;
then A4: dim2 ((P . (len P)),E) = (P . (len P)) `2 by A1, Th51
.= v by A2 ;
deffunc H<sub>1</sub>( set ) -> object = [((P . $1) `1),((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();
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
A7: k in dom Q and
A8: k + 1 in dom Q ; :: thesis: [(Q . k),(Q . (k + 1))] in ==>.-relation TS
( 1 <= k + 1 & k + 1 <= len Q ) by A8, FINSEQ_3:25;
then A9: k + 1 in dom P by A5, FINSEQ_3:25;
( 1 <= k & k <= len Q ) by A7, FINSEQ_3:25;
then A10: k in dom P by A5, FINSEQ_3:25;
then [(P . k),(P . (k + 1))] in ==>.-relation TS by A9, REWRITE1:def 2;
then [[((P . k) `1),((P . k) `2)],(P . (k + 1))] in ==>.-relation TS by A10, A9, Th48;
then [[((P . k) `1),((P . k) `2)],[((P . (k + 1)) `1),((P . (k + 1)) `2)]] in ==>.-relation TS by A10, A9, Th48;
then [[((P . k) `1),(dim2 ((P . k),E))],[((P . (k + 1)) `1),((P . (k + 1)) `2)]] in ==>.-relation TS by A1, A10, Th51;
then [[((P . k) `1),(dim2 ((P . k),E))],[((P . (k + 1)) `1),(dim2 ((P . (k + 1)),E))]] in ==>.-relation TS by A1, A9, Th51;
then (P . k) `1 , dim2 ((P . k),E) ==>. (P . (k + 1)) `1 , dim2 ((P . (k + 1)),E),TS by Def4;
then (P . k) `1 ,(dim2 ((P . k),E)) ^ w ==>. (P . (k + 1)) `1 ,(dim2 ((P . (k + 1)),E)) ^ w,TS by Th25;
then [[((P . k) `1),((dim2 ((P . k),E)) ^ w)],[((P . (k + 1)) `1),((dim2 ((P . (k + 1)),E)) ^ w)]] in ==>.-relation TS by Def4;
then [[((P . k) `1),((dim2 ((P . k),E)) ^ w)],(Q . (k + 1))] in ==>.-relation TS by A6, A8;
hence [(Q . k),(Q . (k + 1))] in ==>.-relation TS by A6, A7; :: thesis: verum

end;

then reconsider Q = Q as RedSequence of ==>.-relation TS by A5, REWRITE1:def 2;
A11: len Q >= 0 + 1 by NAT_1:13;
then len Q in dom Q by FINSEQ_3:25;
then Q . (len Q) = [((P . (len Q)) `1),((dim2 ((P . (len Q)),E)) ^ w)] by A6;
then A12: Q . (len Q) = [y,(v ^ w)] by A2, A5, A4;
1 in dom P by A3, FINSEQ_3:25;
then A13: dim2 ((P . 1),E) = (P . 1) `2 by A1, Th51
.= u by A1 ;
1 in dom Q by A11, FINSEQ_3:25;
then Q . 1 = [((P . 1) `1),((dim2 ((P . 1),E)) ^ w)] by A6
.= [x,(u ^ w)] by A1, A13 ;
hence ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] by A12, REWRITE1:def 3; :: thesis: verum