let x, y be object ; :: thesis: for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
let E be non empty set ; :: thesis: for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
let u be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
let TS be non empty transition-system over F; :: thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y ) )
defpred S₁[ Nat] means for P being RedSequence of ==>.-relation TS
for x, y being object st P . 1 = [x,u] & P . (len P) = [y,u] & len P = $1 holds
not $1 <> 1;
assume A1: not <%> E in rng (dom the Tran of TS) ; :: thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for P being RedSequence of ==>.-relation TS
for x, y being object st P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 holds
not k + 1 <> 1

let P be RedSequence of ==>.-relation TS; :: thesis: for x, y being object st P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 holds
not k + 1 <> 1
let x, y be object ; :: thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 implies not k + 1 <> 1 )
assume that
A3: P . 1 = [x,u] and
A4: P . (len P) = [y,u] and
A5: ( len P = k + 1 & k + 1 <> 1 ) ; :: thesis: contradiction
consider Q being RedSequence of ==>.-relation TS such that
<*(P . 1)*> ^ Q = P and
A6: len P = (len Q) + 1 by A5, Th5, NAT_1:25;
len Q >= 0 + 1 by NAT_1:8;
then (len Q) + 1 >= 1 + 1 by XREAL_1:6;
then A7: 1 + 1 in dom P by A6, FINSEQ_3:25;
len P > 1 by A5, NAT_1:25;
then A8: 1 in dom P by FINSEQ_3:25;
then P . (1 + 1) = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A7, Th48
.= [((P . (1 + 1)) `1),u] by A3, A4, A7, Th54 ;
then [[x,u],[((P . (1 + 1)) `1),u]] in ==>.-relation TS by A3, A8, A7, REWRITE1:def 2;
then x,u ==>. (P . (1 + 1)) `1 ,u,TS by Def4;
hence contradiction by A1, Th28; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

let P be RedSequence of ==>.-relation TS; :: thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] implies ( len P = 1 & x = y ) )
assume A9: ( P . 1 = [x,u] & P . (len P) = [y,u] ) ; :: thesis: ( len P = 1 & x = y )
A10: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A2);
hence len P = 1 by A9; :: thesis: x = y
hence x = y by A9, XTUPLE_0:1; :: thesis: verum