let f be increasing FinSequence of NAT ; :: thesis: for x being Nat st ( for i being Nat st i in dom f holds
f . i < x ) holds
f ^ <*x*> is increasing
let x be Nat; :: thesis: ( ( for i being Nat st i in dom f holds
f . i < x ) implies f ^ <*x*> is increasing )
assume A1: for i being Nat st i in dom f holds
f . i < x ; :: thesis: f ^ <*x*> is increasing
consider k being Nat such that
A2: dom f = Seg k by FINSEQ_1:def 2;
Seg (len f) = Seg k by A2, FINSEQ_1:def 3;
then B2: len f = k by FINSEQ_1:6;
set fn = f ^ <*x*>;
dom (f ^ <*x*>) = Seg ((len f) + (len <*x*>)) by FINSEQ_1:def 7
.= Seg (k + 1) by B2, FINSEQ_1:39 ;
then C4: dom (f ^ <*x*>) = (Seg k) \/ {(k + 1)} by FINSEQ_1:9;
for m, n being Nat st m in dom (f ^ <*x*>) & n in dom (f ^ <*x*>) & m < n holds
(f ^ <*x*>) . m < (f ^ <*x*>) . n

proof

let m, n be Nat; :: thesis: ( m in dom (f ^ <*x*>) & n in dom (f ^ <*x*>) & m < n implies (f ^ <*x*>) . m < (f ^ <*x*>) . n )
assume C1: ( m in dom (f ^ <*x*>) & n in dom (f ^ <*x*>) & m < n ) ; :: thesis: (f ^ <*x*>) . m < (f ^ <*x*>) . n

per cases ( ( m in dom f & n in dom f ) or ( m in dom f & not n in dom f ) or ( not m in dom f & not n in dom f ) or ( not m in dom f & n in dom f ) ) ;

suppose C2: ( m in dom f & n in dom f ) ; :: thesis: (f ^ <*x*>) . m < (f ^ <*x*>) . n

then ( f . m = (f ^ <*x*>) . m & f . n = (f ^ <*x*>) . n ) by FINSEQ_1:def 7;
hence (f ^ <*x*>) . m < (f ^ <*x*>) . n by C2, C1, SEQM_3:def 1; :: thesis: verum

end;

suppose D1: ( m in dom f & not n in dom f ) ; :: thesis: (f ^ <*x*>) . m < (f ^ <*x*>) . n

then n in {(k + 1)} by A2, C1, C4, XBOOLE_0:def 3;
then c3: n = k + 1 by TARSKI:def 1;
f . m = (f ^ <*x*>) . m by D1, FINSEQ_1:def 7;
hence (f ^ <*x*>) . m < (f ^ <*x*>) . n by c3, B2, A1, D1; :: thesis: verum

end;

suppose ( not m in dom f & not n in dom f ) ; :: thesis: (f ^ <*x*>) . m < (f ^ <*x*>) . n

then ( m in {(k + 1)} & n in {(k + 1)} ) by A2, C1, C4, XBOOLE_0:def 3;
then ( m = k + 1 & n = k + 1 ) by TARSKI:def 1;
hence (f ^ <*x*>) . m < (f ^ <*x*>) . n by C1; :: thesis: verum

end;

suppose D1: ( not m in dom f & n in dom f ) ; :: thesis: (f ^ <*x*>) . m < (f ^ <*x*>) . n

then m in {(k + 1)} by A2, C1, C4, XBOOLE_0:def 3;
then C4: m = k + 1 by TARSKI:def 1;
n <= k by A2, D1, FINSEQ_1:1;
hence (f ^ <*x*>) . m < (f ^ <*x*>) . n by C1, C4, NAT_1:13; :: thesis: verum

end;

end;

end;

hence f ^ <*x*> is increasing by SEQM_3:def 1; :: thesis: verum