let p, q be real-valued increasing FinSequence; :: thesis: ( p . (len p) < q . 1 implies p ^ q is increasing )
set pq = p ^ q;

per cases ( p is empty or q is empty or ( not p is empty & not q is empty ) ) ;

suppose ( p is empty or q is empty ) ; :: thesis: ( p . (len p) < q . 1 implies p ^ q is increasing )

hence ( p . (len p) < q . 1 implies p ^ q is increasing ) by FINSEQ_1:34; :: thesis: verum

end;

suppose that A1: not p is empty and
A2: not q is empty ; :: thesis: ( p . (len p) < q . 1 implies p ^ q is increasing )

assume A3: p . (len p) < q . 1 ; :: thesis: p ^ q is increasing
let e1, e2 be Nat; :: according to SEQM_3:def 1 :: thesis: ( not e1 in proj1 (p ^ q) or not e2 in proj1 (p ^ q) or e2 <= e1 or not (p ^ q) . e2 <= (p ^ q) . e1 )
assume that
A4: e1 in dom (p ^ q) and
A5: e2 in dom (p ^ q) and
A6: e1 < e2 ; :: thesis: not (p ^ q) . e2 <= (p ^ q) . e1

per cases ( ( e1 in dom p & e2 in dom p ) or ( e1 in dom p & ex n being Nat st
( n in dom q & e2 = (len p) + n ) ) or ( ex n being Nat st
( n in dom q & e1 = (len p) + n ) & e2 in dom p ) or ( ex n being Nat st
( n in dom q & e1 = (len p) + n ) & ex n being Nat st
( n in dom q & e2 = (len p) + n ) ) ) by A4, A5, FINSEQ_1:25;

suppose A7: ( e1 in dom p & e2 in dom p ) ; :: thesis: not (p ^ q) . e2 <= (p ^ q) . e1

then ( (p ^ q) . e1 = p . e1 & (p ^ q) . e2 = p . e2 ) by FINSEQ_1:def 7;
hence (p ^ q) . e1 < (p ^ q) . e2 by A6, A7, VALUED_0:def 13; :: thesis: verum

end;

suppose A8: ( e1 in dom p & ex n being Nat st
( n in dom q & e2 = (len p) + n ) ) ; :: thesis: not (p ^ q) . e2 <= (p ^ q) . e1

then consider n0 being Nat such that
A9: n0 in dom q and
A10: e2 = (len p) + n0 ;
A11: ( (p ^ q) . e1 = p . e1 & (p ^ q) . e2 = q . n0 ) by A8, A10, FINSEQ_1:def 7;
rng q <> {} by A2;
then A12: 1 in dom q by FINSEQ_3:32;
1 <= n0 by A9, FINSEQ_3:25;
then ( 1 = n0 or 1 < n0 ) by XXREAL_0:1;
then A13: q . 1 <= q . n0 by A9, A12, VALUED_0:def 13;
rng p <> {} by A1;
then 1 in dom p by FINSEQ_3:32;
then 1 <= len p by FINSEQ_3:25;
then A14: len p in dom p by FINSEQ_3:25;
e1 <= len p by A8, FINSEQ_3:25;
then ( e1 < len p or e1 = len p ) by XXREAL_0:1;
then p . e1 <= p . (len p) by A14, A8, VALUED_0:def 13;
then p . e1 < q . 1 by A3, XXREAL_0:2;
hence (p ^ q) . e1 < (p ^ q) . e2 by A11, A13, XXREAL_0:2; :: thesis: verum

end;

suppose A15: ( ex n being Nat st
( n in dom q & e1 = (len p) + n ) & e2 in dom p ) ; :: thesis: not (p ^ q) . e2 <= (p ^ q) . e1

then consider n0 being Nat such that
n0 in dom q and
A16: e1 = (len p) + n0 ;
A17: len p <= e1 by A16, NAT_1:11;
e2 in Seg (len p) by A15, FINSEQ_1:def 3;
then e2 <= len p by FINSEQ_1:1;
hence (p ^ q) . e1 < (p ^ q) . e2 by A6, A17, XXREAL_0:2; :: thesis: verum

end;

suppose A18: ( ex n being Nat st
( n in dom q & e1 = (len p) + n ) & ex n being Nat st
( n in dom q & e2 = (len p) + n ) ) ; :: thesis: not (p ^ q) . e2 <= (p ^ q) . e1

then consider n1 being Nat such that
A19: n1 in dom q and
A20: e1 = (len p) + n1 ;
consider n2 being Nat such that
A21: n2 in dom q and
A22: e2 = (len p) + n2 by A18;
A23: ((len p) + n1) - (len p) < ((len p) + n2) - (len p) by A6, A20, A22, XREAL_1:14;
( q . n1 = (p ^ q) . e1 & q . n2 = (p ^ q) . e2 ) by A19, A20, A21, A22, FINSEQ_1:def 7;
hence (p ^ q) . e1 < (p ^ q) . e2 by A23, A19, A21, VALUED_0:def 13; :: thesis: verum

end;

end;

end;

end;