let s, t be non empty increasing FinSequence of REAL ; :: thesis: ( s . (len s) < t . 1 implies s ^ t is non empty increasing FinSequence of REAL )
assume A1: s . (len s) < t . 1 ; :: thesis: s ^ t is non empty increasing FinSequence of REAL
set H = s ^ t;
A2: len (s ^ t) = (len s) + (len t) by FINSEQ_1:22;
for e1, e2 being ExtReal st e1 in dom (s ^ t) & e2 in dom (s ^ t) & e1 < e2 holds
(s ^ t) . e1 < (s ^ t) . e2

proof

let e1, e2 be ExtReal; :: thesis: ( e1 in dom (s ^ t) & e2 in dom (s ^ t) & e1 < e2 implies (s ^ t) . e1 < (s ^ t) . e2 )
assume A3: ( e1 in dom (s ^ t) & e2 in dom (s ^ t) & e1 < e2 ) ; :: thesis: (s ^ t) . e1 < (s ^ t) . e2
then reconsider ie1 = e1, ie2 = e2 as Nat ;
A5: ( 1 <= ie1 & ie1 <= (len s) + (len t) & 1 <= ie2 & ie2 <= (len s) + (len t) ) by A2, A3, FINSEQ_3:25;

per cases ( ie2 <= len s or len s < ie2 ) ;

suppose A6: ie2 <= len s ; :: thesis: (s ^ t) . e1 < (s ^ t) . e2

then A7: ie1 <= len s by A3, XXREAL_0:2;
A8: ( ie1 in dom s & ie2 in dom s ) by A5, A6, A7, FINSEQ_3:25;
then ( (s ^ t) . e1 = s . e1 & (s ^ t) . e2 = s . e2 ) by FINSEQ_1:def 7;
hence (s ^ t) . e1 < (s ^ t) . e2 by A3, A8, VALUED_0:def 13; :: thesis: verum

end;

suppose A9: len s < ie2 ; :: thesis: (s ^ t) . e1 < (s ^ t) . e2

per cases ( len s < ie1 or ie1 <= len s ) ;

suppose A10: len s < ie1 ; :: thesis: (s ^ t) . e1 < (s ^ t) . e2

then a10: len s < ie2 by A3, XXREAL_0:2;
A11: ( not ie1 in dom s & not ie2 in dom s ) by A10, FINSEQ_3:25, a10;
then consider n1 being Nat such that
A12: ( n1 in dom t & ie1 = (len s) + n1 ) by A3, FINSEQ_1:25;
consider n2 being Nat such that
A13: ( n2 in dom t & ie2 = (len s) + n2 ) by A3, A11, FINSEQ_1:25;
A14: (s ^ t) . e1 = t . n1 by A12, FINSEQ_1:def 7;
A15: (s ^ t) . e2 = t . n2 by A13, FINSEQ_1:def 7;
ie1 - (len s) < ie2 - (len s) by A3, XREAL_1:14;
hence (s ^ t) . e1 < (s ^ t) . e2 by A12, A13, A14, A15, VALUED_0:def 13; :: thesis: verum

end;

suppose A16: ie1 <= len s ; :: thesis: (s ^ t) . e1 < (s ^ t) . e2

not ie2 in dom s by FINSEQ_3:25, A9;
then consider n2 being Nat such that
A17: ( n2 in dom t & ie2 = (len s) + n2 ) by A3, FINSEQ_1:25;
A18: ( 1 <= n2 & n2 <= len t ) by A17, FINSEQ_3:25;
1 <= len t by A18, XXREAL_0:2;
then 1 in dom t by FINSEQ_3:25;
then A19: t . 1 <= t . n2 by A17, A18, VALUED_0:def 15;
A20: (s ^ t) . e2 = t . n2 by A17, FINSEQ_1:def 7;
A21: ie1 in dom s by A5, A16, FINSEQ_3:25;
then A22: (s ^ t) . e1 = s . ie1 by FINSEQ_1:def 7;
len s in Seg (len s) by FINSEQ_1:3;
then len s in dom s by FINSEQ_1:def 3;
then s . ie1 <= s . (len s) by A16, A21, VALUED_0:def 15;
then s . ie1 < t . 1 by A1, XXREAL_0:2;
hence (s ^ t) . e1 < (s ^ t) . e2 by A19, A20, A22, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

hence s ^ t is non empty increasing FinSequence of REAL by VALUED_0:def 13; :: thesis: verum