let I be set ; :: thesis: for R being asymmetric Relation of I
for p, q, r being I -valued FinSequence holds
( [p,q] in LexOrder (I,R) iff [(r ^ p),(r ^ q)] in LexOrder (I,R) )
let R be asymmetric Relation of I; :: thesis: for p, q, r being I -valued FinSequence holds
( [p,q] in LexOrder (I,R) iff [(r ^ p),(r ^ q)] in LexOrder (I,R) )
let p, q, r be I -valued FinSequence; :: thesis: ( [p,q] in LexOrder (I,R) iff [(r ^ p),(r ^ q)] in LexOrder (I,R) )

hereby :: thesis: ( [(r ^ p),(r ^ q)] in LexOrder (I,R) implies [p,q] in LexOrder (I,R) )

assume [p,q] in LexOrder (I,R) ; :: thesis: [(r ^ p),(r ^ q)] in LexOrder (I,R)

per cases then ( p c< q or ex k being Nat st
( k in dom p & k in dom q & [(p . k),(q . k)] in R & ( for n being Nat st 1 <= n & n < k holds
p . n = q . n ) ) ) by LO;

suppose p c< q ; :: thesis: [(r ^ p),(r ^ q)] in LexOrder (I,R)

then ( r ^ p c= r ^ q & r ^ p <> r ^ q ) by FINSEQ_6:13, FINSEQ_1:33, XBOOLE_0:def 8;
then r ^ p c< r ^ q by XBOOLE_0:def 8;
hence [(r ^ p),(r ^ q)] in LexOrder (I,R) by LO; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom p & k in dom q & [(p . k),(q . k)] in R & ( for n being Nat st 1 <= n & n < k holds
p . n = q . n ) ) ; :: thesis: [(r ^ p),(r ^ q)] in LexOrder (I,R)

then consider k being Nat such that
A1: ( k in dom p & k in dom q & [(p . k),(q . k)] in R & ( for n being Nat st 1 <= n & n < k holds
p . n = q . n ) ) ;
set i = len r;
set j = (len r) + k;
A2: ( (len r) + k in dom (r ^ p) & (len r) + k in dom (r ^ q) ) by A1, FINSEQ_1:28;
A3: ( (r ^ p) . ((len r) + k) = p . k & (r ^ q) . ((len r) + k) = q . k ) by A1, FINSEQ_1:def 7;
for n being Nat st 1 <= n & n < (len r) + k holds
(r ^ p) . n = (r ^ q) . n

proof

let n be Nat; :: thesis: ( 1 <= n & n < (len r) + k implies (r ^ p) . n = (r ^ q) . n )
assume A4: ( 1 <= n & n < (len r) + k ) ; :: thesis: (r ^ p) . n = (r ^ q) . n

per cases ( n <= len r or (len r) + 1 <= n ) by NAT_1:13;

suppose n <= len r ; :: thesis: (r ^ p) . n = (r ^ q) . n

then n in dom r by A4, FINSEQ_3:25;
then ( (r ^ p) . n = r . n & r . n = (r ^ q) . n ) by FINSEQ_1:def 7;
hence (r ^ p) . n = (r ^ q) . n ; :: thesis: verum

end;

suppose (len r) + 1 <= n ; :: thesis: (r ^ p) . n = (r ^ q) . n

then consider m being Nat such that
A5: n = ((len r) + 1) + m by NAT_1:10;
A5A: n = (len r) + (1 + m) by A5;
then A6: ( 1 <= 1 + m & 1 + m < k ) by A4, NAT_1:11, XREAL_1:6;
( k <= len p & k <= len q ) by A1, FINSEQ_3:25;
then ( 1 <= 1 + m & 1 + m <= len p & 1 + m <= len q ) by A6, XXREAL_0:2;
then ( 1 + m in dom p & 1 + m in dom q ) by FINSEQ_3:25;
then ( (r ^ p) . n = p . (1 + m) & (r ^ q) . n = q . (1 + m) ) by A5A, FINSEQ_1:def 7;
hence (r ^ p) . n = (r ^ q) . n by A1, A6; :: thesis: verum

end;

end;

end;

hence [(r ^ p),(r ^ q)] in LexOrder (I,R) by LO, A1, A2, A3; :: thesis: verum

end;

end;

end;

assume [(r ^ p),(r ^ q)] in LexOrder (I,R) ; :: thesis: [p,q] in LexOrder (I,R)

per cases then ( r ^ p c< r ^ q or ex k being Nat st
( k in dom (r ^ p) & k in dom (r ^ q) & [((r ^ p) . k),((r ^ q) . k)] in R & ( for n being Nat st 1 <= n & n < k holds
(r ^ p) . n = (r ^ q) . n ) ) ) by LO;

suppose r ^ p c< r ^ q ; :: thesis: [p,q] in LexOrder (I,R)

then p c< q by Lem13;
hence [p,q] in LexOrder (I,R) by LO; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom (r ^ p) & k in dom (r ^ q) & [((r ^ p) . k),((r ^ q) . k)] in R & ( for n being Nat st 1 <= n & n < k holds
(r ^ p) . n = (r ^ q) . n ) ) ; :: thesis: [p,q] in LexOrder (I,R)

then consider k being Nat such that
A1: ( k in dom (r ^ p) & k in dom (r ^ q) & [((r ^ p) . k),((r ^ q) . k)] in R & ( for n being Nat st 1 <= n & n < k holds
(r ^ p) . n = (r ^ q) . n ) ) ;
set i = len r;
A3: 1 <= k by A1, FINSEQ_3:25;

now :: thesis: not k <= len r

assume k <= len r ; :: thesis: contradiction
then k in dom r by A3, FINSEQ_3:25;
then ( (r ^ p) . k = r . k & r . k = (r ^ q) . k ) by FINSEQ_1:def 7;
hence contradiction by A1, PREFER_1:22; :: thesis: verum

end;

then k >= (len r) + 1 by NAT_1:13;
then consider j being Nat such that
A4: k = ((len r) + 1) + j by NAT_1:10;
A5: k = (len r) + (1 + j) by A4;
( k <= len (r ^ p) & len (r ^ p) = (len r) + (len p) & k <= len (r ^ q) & len (r ^ q) = (len r) + (len q) ) by A1, FINSEQ_3:25, FINSEQ_1:22;
then A9: ( 1 <= 1 + j & 1 + j <= len p & 1 + j <= len q ) by A5, NAT_1:11, XREAL_1:6;
then A6: ( 1 + j in dom p & 1 + j in dom q ) by FINSEQ_3:25;
then A7: ( (r ^ p) . k = p . (1 + j) & (r ^ q) . k = q . (1 + j) ) by A5, FINSEQ_1:def 7;
for n being Nat st 1 <= n & n < 1 + j holds
p . n = q . n

proof

let n be Nat; :: thesis: ( 1 <= n & n < 1 + j implies p . n = q . n )
assume A8: ( 1 <= n & n < 1 + j ) ; :: thesis: p . n = q . n
then ( n < len p & n < len q ) by A9, XXREAL_0:2;
then ( n in dom p & n in dom q ) by A8, FINSEQ_3:25;
then ( p . n = (r ^ p) . ((len r) + n) & q . n = (r ^ q) . ((len r) + n) & 1 <= (len r) + n & (len r) + n < k ) by FINSEQ_1:def 7, NAT_1:12, XREAL_1:6, A5, A8;
hence p . n = q . n by A1; :: thesis: verum

end;

hence [p,q] in LexOrder (I,R) by LO, A1, A6, A7; :: thesis: verum

end;

end;