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: now

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

end;

then A7: rng f c= rng (g | N) by TARSKI:def 3;
rng (g | N) c= rng g by RELAT_1:99;
hence rng f c= rng g by A7, 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 A2, TARSKI:def 3; :: thesis: verum