let p, q be non empty increasing FinSequence of REAL ; :: thesis: ( p . (len p) < q . 1 implies p ^ q is non empty increasing FinSequence of REAL )
assume A1: p . (len p) < q . 1 ; :: thesis: p ^ q is non empty increasing FinSequence of REAL
set pq = p ^ q;

now :: thesis: for e1, e2 being ExtReal st e1 in dom (p ^ q) & e2 in dom (p ^ q) & e1 < e2 holds
(p ^ q) . e1 < (p ^ q) . e2

let e1, e2 be ExtReal; :: thesis: ( e1 in dom (p ^ q) & e2 in dom (p ^ q) & e1 < e2 implies (p ^ q) . b₁ < (p ^ q) . b₂ )
assume that
A2: e1 in dom (p ^ q) and
A3: e2 in dom (p ^ q) and
A4: e1 < e2 ; :: thesis: (p ^ q) . b₁ < (p ^ q) . b₂

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 A2, A3, FINSEQ_1:25;

suppose A5: ( e1 in dom p & e2 in dom p ) ; :: thesis: (p ^ q) . b₁ < (p ^ q) . b₂

then A6: ( (p ^ q) . e1 = p . e1 & (p ^ q) . e2 = p . e2 ) by FINSEQ_1:def 7;
( e1 < e2 & p is increasing ) by A4;
hence (p ^ q) . e1 < (p ^ q) . e2 by A5, A6; :: thesis: verum

end;

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

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

end;

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

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

end;

suppose A17: ( 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: (p ^ q) . b₁ < (p ^ q) . b₂

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

end;

end;

end;

then p ^ q is increasing ;
hence p ^ q is non empty increasing FinSequence of REAL ; :: thesis: verum