let q be FinSubsequence; :: thesis: ex p being FinSequence st q c= p
consider k being Nat such that
A1: dom q c= Seg k by FINSEQ_1:def 12;
reconsider IK = id (Seg k) as Function ;
set IS = IK +* q;
dom (IK +* q) = (dom IK) \/ (dom q) by FUNCT_4:def 1
.= (Seg k) \/ (dom q)
.= Seg k by A1, 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 ; :: thesis: verum