let p, q, r be FinSequence; :: thesis: ( r ^ p c< r ^ q iff p c< q )
thus ( r ^ p c< r ^ q implies p c< q ) :: thesis: ( p c< q implies r ^ p c< r ^ q )

proof

assume A0: r ^ p c< r ^ q ; :: thesis: p c< q
( len (r ^ p) = (len r) + (len p) & len (r ^ q) = (len r) + (len q) ) by FINSEQ_1:22;
then A2: len p < len q by A0, Lem12, XREAL_1:6;
then A3: dom p c= dom q by FINSEQ_3:30;
for i being Nat st i in dom p holds
p . i = q . i

proof

let i be Nat; :: thesis: ( i in dom p implies p . i = q . i )
assume i in dom p ; :: thesis: p . i = q . i
then ( p . i = (r ^ p) . ((len r) + i) & q . i = (r ^ q) . ((len r) + i) & (len r) + i in dom (r ^ p) ) by A3, FINSEQ_1:def 7, FINSEQ_1:28;
hence p . i = q . i by A0, Lem12; :: thesis: verum

end;

hence p c< q by A2, Lem12; :: thesis: verum

end;

assume p c< q ; :: thesis: r ^ p c< r ^ q
then ( r ^ p c= r ^ q & r ^ p <> r ^ q ) by FINSEQ_6:13, FINSEQ_1:33, XBOOLE_0:def 8;
hence r ^ p c< r ^ q by XBOOLE_0:def 8; :: thesis: verum