let x, y be set ; :: 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 of 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 of 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 of 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 of 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 of 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 ) )
assume A: 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 )
defpred S₁[ Nat] means for P being RedSequence of ==>.-relation TS
for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = $1 holds
not $1 <> 1;
C: S₁[ 0 ] ;

D: now

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

now

let P be RedSequence of ==>.-relation TS; :: thesis: for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 holds
not k + 1 <> 1
let x, y be set ; :: thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 implies not k + 1 <> 1 )
assume that
D1: ( P . 1 = [x,u] & P . (len P) = [y,u] ) and
D2: ( len P = k + 1 & k + 1 <> 1 ) ; :: thesis: contradiction
D2'A: len P > 1 by D2, NAT_1:26;
consider Q being RedSequence of ==>.-relation TS such that
D3: ( <*(P . 1)*> ^ Q = P & len P = (len Q) + 1 ) by D2, LmRed10, NAT_1:26;
D4'A: len Q >= 0 + 1 by NAT_1:8;
(len Q) + 1 >= 1 + 1 by D4'A, XREAL_1:8;
then D5: ( 1 in dom P & 1 + 1 in dom P ) by D2'A, D3, FINSEQ_3:27;
then P . (1 + 1) = [((P . (1 + 1)) `1 ),((P . (1 + 1)) `2 )] by ThRedSeq5
.= [((P . (1 + 1)) `1 ),u] by D1, D5, ThRedSeq70 ;
then [[x,u],[((P . (1 + 1)) `1 ),u]] in ==>.-relation TS by D1, D5, REWRITE1:def 2;
then x,u ==>. (P . (1 + 1)) `1 ,u,TS by DefRel;
hence contradiction by A, ThDir60; :: thesis: verum

end;

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

end;

E: for k being Nat holds S₁[k] from NAT_1:sch 2(C, D);
let P be RedSequence of ==>.-relation TS; :: thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] implies ( len P = 1 & x = y ) )
assume F: ( P . 1 = [x,u] & P . (len P) = [y,u] ) ; :: thesis: ( len P = 1 & x = y )
thus G: len P = 1 by E, F; :: thesis: x = y
thus x = y by F, G, ZFMISC_1:33; :: thesis: verum