let q be FinSubsequence; :: thesis: for k, n being Element of NAT st dom q c= Seg k & n > k holds
ex p being FinSequence st
( q c= p & dom p = Seg n )
let k, n be Element of NAT ; :: thesis: ( dom q c= Seg k & n > k implies ex p being FinSequence st
( q c= p & dom p = Seg n ) )
assume that
A1: dom q c= Seg k and
A2: n > k ; :: thesis: ex p being FinSequence st
( q c= p & dom p = Seg n )
reconsider IK = id (Seg n) as Function ;
set IS = IK +* q;
A3: Seg k c= Seg n by A2, FINSEQ_1:5;
A4: dom (IK +* q) = (dom IK) \/ (dom q) by FUNCT_4:def 1
.= (Seg n) \/ (dom q)
.= Seg n by A1, A3, XBOOLE_1:1, XBOOLE_1:12 ;
then reconsider IS = IK +* q as FinSequence by FINSEQ_1:def 2;
q c= IS by FUNCT_4:25;
hence ex p being FinSequence st
( q c= p & dom p = Seg n ) by A4; :: thesis: verum