let f, g be FinSequence of CQC-WFF ; :: thesis: ( f is_Subsequence_of g implies ( rng f c= rng g & ex N being Subset of NAT st rng f c= rng (g | N) ) )
assume f is_Subsequence_of g ; :: thesis: ( rng f c= rng g & ex N being Subset of NAT st rng f c= rng (g | N) )
then consider N being Subset of NAT such that
A1: f c= Seq (g | N) by Def4;
A2: rng (g | N) c= rng g by RELAT_1:70;

A3: now

rng (Seq (g | N)) = rng ((g | N) * (Sgm (dom (g | N)))) by FINSEQ_1:def 14;
then A4: rng (Seq (g | N)) c= rng (g | N) by RELAT_1:26;
let a be set ; :: thesis: ( a in rng f implies a in rng (g | N) )
assume a in rng f ; :: thesis: a in rng (g | N)
then consider n being Nat such that
A5: n in dom f and
A6: f . n = a by FINSEQ_2:10;
[n,(f . n)] in f by A5, FUNCT_1:1;
then A7: (Seq (g | N)) . n = a by A1, A6, FUNCT_1:1;
dom f c= dom (Seq (g | N)) by A1, RELAT_1:11;
then a in rng (Seq (g | N)) by A5, A7, FUNCT_1:3;
hence a in rng (g | N) by A4; :: thesis: verum

end;

then rng f c= rng (g | N) by TARSKI:def 3;
hence rng f c= rng g by A2, XBOOLE_1:1; :: thesis: ex N being Subset of NAT st rng f c= rng (g | N)
take N ; :: thesis: rng f c= rng (g | N)
thus rng f c= rng (g | N) by A3, TARSKI:def 3; :: thesis: verum