let E be non empty set ; :: thesis: for u, v being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v )

let u, v be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v )

let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; :: thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v )

defpred S_{1}[ Nat] means for R being RedSequence of ==>.-relation TS

for u being Element of E ^omega st len R = $1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v );

_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A19, A1);

hence for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v ) ; :: thesis: verum

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v )

let u, v be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v )

let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; :: thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v )

defpred S

for u being Element of E ^omega st len R = $1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v );

A1: now :: thesis: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

A19:
SS

let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A2: S_{1}[i]
; :: thesis: S_{1}[i + 1]

thus S_{1}[i + 1]
:: thesis: verum

end;assume A2: S

thus S

proof

let R be RedSequence of ==>.-relation TS; :: thesis: for u being Element of E ^omega st len R = i + 1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v )

let u be Element of E ^omega ; :: thesis: ( len R = i + 1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E implies ex l being Nat st

( l in dom R & (R . l) `2 = v ) )

assume that

A3: len R = i + 1 and

A4: (R . 1) `2 = u ^ v and

A5: (R . (len R)) `2 = <%> E ; :: thesis: ex l being Nat st

( l in dom R & (R . l) `2 = v )

end;ex l being Nat st

( l in dom R & (R . l) `2 = v )

let u be Element of E ^omega ; :: thesis: ( len R = i + 1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E implies ex l being Nat st

( l in dom R & (R . l) `2 = v ) )

assume that

A3: len R = i + 1 and

A4: (R . 1) `2 = u ^ v and

A5: (R . (len R)) `2 = <%> E ; :: thesis: ex l being Nat st

( l in dom R & (R . l) `2 = v )

per cases
( len u = 0 or len u > 0 )
;

end;

suppose A6:
len u = 0
; :: thesis: ex l being Nat st

( l in dom R & (R . l) `2 = v )

( l in dom R & (R . l) `2 = v )

set j = 1;

take 1 ; :: thesis: ( 1 in dom R & (R . 1) `2 = v )

rng R <> {} ;

hence 1 in dom R by FINSEQ_3:32; :: thesis: (R . 1) `2 = v

u = {} by A6;

hence (R . 1) `2 = v by A4; :: thesis: verum

end;take 1 ; :: thesis: ( 1 in dom R & (R . 1) `2 = v )

rng R <> {} ;

hence 1 in dom R by FINSEQ_3:32; :: thesis: (R . 1) `2 = v

u = {} by A6;

hence (R . 1) `2 = v by A4; :: thesis: verum

suppose A7:
len u > 0
; :: thesis: ex l being Nat st

( l in dom R & (R . l) `2 = v )

( l in dom R & (R . l) `2 = v )

then consider e being Element of E, u1 being Element of E ^omega such that

A8: u = <%e%> ^ u1 by Th7;

len u >= 0 + 1 by A7, NAT_1:13;

then (len u) + (len v) >= 1 + (len v) by XREAL_1:6;

then len (u ^ v) >= 1 + (len v) by AFINSQ_1:17;

then len (u ^ v) >= 1 by Th1;

then (len R) + (len (u ^ v)) > (len (u ^ v)) + 1 by A4, A5, Th23, XREAL_1:8;

then len R > 1 by XREAL_1:6;

then consider R9 being RedSequence of ==>.-relation TS such that

A9: (len R9) + 1 = len R and

A10: for k being Nat st k in dom R9 holds

R9 . k = R . (k + 1) by REWRITE3:7;

A11: rng R9 <> {} ;

then A12: (R9 . 1) `2 = (R . (1 + 1)) `2 by A10, FINSEQ_3:32;

1 in dom R9 by A11, FINSEQ_3:32;

then 1 <= len R9 by FINSEQ_3:25;

then len R9 in dom R9 by FINSEQ_3:25;

then A13: (R9 . (len R9)) `2 = <%> E by A5, A9, A10;

A14: (R . 1) `2 = <%e%> ^ (u1 ^ v) by A4, A8, AFINSQ_1:27;

thus ex k being Nat st

( k in dom R & (R . k) `2 = v ) :: thesis: verum

end;A8: u = <%e%> ^ u1 by Th7;

len u >= 0 + 1 by A7, NAT_1:13;

then (len u) + (len v) >= 1 + (len v) by XREAL_1:6;

then len (u ^ v) >= 1 + (len v) by AFINSQ_1:17;

then len (u ^ v) >= 1 by Th1;

then (len R) + (len (u ^ v)) > (len (u ^ v)) + 1 by A4, A5, Th23, XREAL_1:8;

then len R > 1 by XREAL_1:6;

then consider R9 being RedSequence of ==>.-relation TS such that

A9: (len R9) + 1 = len R and

A10: for k being Nat st k in dom R9 holds

R9 . k = R . (k + 1) by REWRITE3:7;

A11: rng R9 <> {} ;

then A12: (R9 . 1) `2 = (R . (1 + 1)) `2 by A10, FINSEQ_3:32;

1 in dom R9 by A11, FINSEQ_3:32;

then 1 <= len R9 by FINSEQ_3:25;

then len R9 in dom R9 by FINSEQ_3:25;

then A13: (R9 . (len R9)) `2 = <%> E by A5, A9, A10;

A14: (R . 1) `2 = <%e%> ^ (u1 ^ v) by A4, A8, AFINSQ_1:27;

thus ex k being Nat st

( k in dom R & (R . k) `2 = v ) :: thesis: verum

proof
end;

per cases
( (R . 2) `2 = u ^ v or (R . 2) `2 = u1 ^ v )
by A4, A5, A14, Th22;

end;

suppose
(R . 2) `2 = u ^ v
; :: thesis: ex k being Nat st

( k in dom R & (R . k) `2 = v )

( k in dom R & (R . k) `2 = v )

then consider l being Nat such that

A15: l in dom R9 and

A16: (R9 . l) `2 = v by A2, A3, A9, A12, A13;

set k = l + 1;

take l + 1 ; :: thesis: ( l + 1 in dom R & (R . (l + 1)) `2 = v )

thus l + 1 in dom R by A9, A15, Th3; :: thesis: (R . (l + 1)) `2 = v

thus (R . (l + 1)) `2 = v by A10, A15, A16; :: thesis: verum

end;A15: l in dom R9 and

A16: (R9 . l) `2 = v by A2, A3, A9, A12, A13;

set k = l + 1;

take l + 1 ; :: thesis: ( l + 1 in dom R & (R . (l + 1)) `2 = v )

thus l + 1 in dom R by A9, A15, Th3; :: thesis: (R . (l + 1)) `2 = v

thus (R . (l + 1)) `2 = v by A10, A15, A16; :: thesis: verum

suppose
(R . 2) `2 = u1 ^ v
; :: thesis: ex k being Nat st

( k in dom R & (R . k) `2 = v )

( k in dom R & (R . k) `2 = v )

then consider l being Nat such that

A17: l in dom R9 and

A18: (R9 . l) `2 = v by A2, A3, A9, A12, A13;

set k = l + 1;

take l + 1 ; :: thesis: ( l + 1 in dom R & (R . (l + 1)) `2 = v )

thus l + 1 in dom R by A9, A17, Th3; :: thesis: (R . (l + 1)) `2 = v

thus (R . (l + 1)) `2 = v by A10, A17, A18; :: thesis: verum

end;A17: l in dom R9 and

A18: (R9 . l) `2 = v by A2, A3, A9, A12, A13;

set k = l + 1;

take l + 1 ; :: thesis: ( l + 1 in dom R & (R . (l + 1)) `2 = v )

thus l + 1 in dom R by A9, A17, Th3; :: thesis: (R . (l + 1)) `2 = v

thus (R . (l + 1)) `2 = v by A10, A17, A18; :: thesis: verum

for k being Nat holds S

hence for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v ) ; :: thesis: verum