let E be non empty set ; :: 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
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
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
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
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
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2 )
assume A: not <%> E in rng (dom the Tran of TS) ; :: thesis: for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
defpred S₁[ Nat] means for P being RedSequence of ==>.-relation TS
for k, l being Nat st len P = $1 & k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2 ;
B: S₁[ 0 ] ;

C: now

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

now

let P be RedSequence of ==>.-relation TS; :: thesis: for k, l being Nat st len P = i + 1 & k in dom P & l in dom P & k < l holds
(b₃ . b₄) `2 <> (b<sub>3</sub> . b<sub>5</sub>) `2
let k, l be Nat; :: thesis: ( len P = i + 1 & k in dom P & l in dom P & k < l implies (b₁ . b₂) `2 <> (b<sub>1</sub> . b<sub>3</sub>) `2 )
assume D1: ( len P = i + 1 & k in dom P & l in dom P & k < l ) ; :: thesis: (b₁ . b₂) `2 <> (b<sub>1</sub> . b<sub>3</sub>) `2
D2: i < len P by D1, NAT_1:13;
D3: ( 1 <= k & k <= len P & 1 <= l & l <= len P ) by D1, FINSEQ_3:27;

per cases ( ( k = 1 & l = len P ) or ( k <> 1 & l = len P ) or l <> len P ) ;

suppose ( k = 1 & l = len P ) ; :: thesis: (b₁ . b₂) `2 <> (b<sub>1</sub> . b<sub>3</sub>) `2

hence (P . k) `2 <> (P . l) `2 by A, D1, ThRedSeq81; :: thesis: verum

end;

suppose E: ( k <> 1 & l = len P ) ; :: thesis: (b₁ . b₂) `2 <> (b<sub>1</sub> . b<sub>3</sub>) `2

then E0'a: k > 1 by D3, XXREAL_0:1;
E0'b: l > 1 by D3, D1, XXREAL_0:1;
then consider Q being RedSequence of ==>.-relation TS such that
E0: ( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) by E, LmRed10;
E0': len <*(P . 1)*> = 1 by FINSEQ_1:57;
reconsider k1 = k - 1 as Nat by D3, NAT_1:21;
reconsider l1 = l - 1 as Nat by D3, NAT_1:21;
k1 > 1 - 1 by E0'a, XREAL_1:11;
then E2'a: k1 >= 0 + 1 by NAT_1:13;
l1 > 1 - 1 by E0'b, XREAL_1:11;
then E2'b: l1 >= 0 + 1 by NAT_1:13;
E2'c: k1 <= ((len Q) + 1) - 1 by D3, E0, XREAL_1:11;
E2'd: l1 <= ((len Q) + 1) - 1 by D3, E0, XREAL_1:11;
E3: ( k1 in dom Q & l1 in dom Q ) by E2'a, E2'b, E2'c, E2'd, FINSEQ_3:27;
E4: k1 < l1 by D1, XREAL_1:11;
( P . k = Q . k1 & P . l = Q . l1 ) by D3, E0, E0', E0'a, E0'b, FINSEQ_1:37;
hence (P . k) `2 <> (P . l) `2 by D, D1, E0, E3, E4; :: thesis: verum

end;

suppose l <> len P ; :: thesis: (b₁ . b₂) `2 <> (b<sub>1</sub> . b<sub>3</sub>) `2

then l < i + 1 by D1, D3, XXREAL_0:1;
then ( k < i + 1 & l <= i ) by D1, NAT_1:13, XXREAL_0:2;
then E0: ( k <= i & l <= i ) by NAT_1:13;
then reconsider Q = P | i as RedSequence of ==>.-relation TS by D3, REWRITE2:3, XXREAL_0:2;
E0'a: ( k <= len Q & l <= len Q ) by D2, E0, FINSEQ_1:80;
E1: len Q = i by D2, FINSEQ_1:80;
E2: k in dom Q by D3, E0'a, FINSEQ_3:27;
E3: l in dom Q by D3, E0'a, FINSEQ_3:27;
( P . k = Q . k & P . l = Q . l ) by E0, FINSEQ_3:121;
hence (P . k) `2 <> (P . l) `2 by D, D1, E1, E2, E3; :: thesis: verum

end;

end;

end;

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

end;

D: for i being Nat holds S₁[i] from NAT_1:sch 2(B, C);
let P be RedSequence of ==>.-relation TS; :: thesis: for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
let k, l be Nat; :: thesis: ( k in dom P & l in dom P & k < l implies (P . k) `2 <> (P . l) `2 )
assume E: ( k in dom P & l in dom P & k < l ) ; :: thesis: (P . k) `2 <> (P . l) `2
len P = len P ;
hence (P . k) `2 <> (P . l) `2 by D, E; :: thesis: verum