let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al st f is_Subsequence_of g holds
( rng f c= rng g & ex N being Subset of NAT st rng f c= rng (g | N) )
let f, g be FinSequence of CQC-WFF Al; :: 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) ;
A2: rng (g | N) c= rng g by RELAT_1:70;
A3: now :: thesis: for a being object st a in rng f holds
a in rng (g | N)
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 object ; :: 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) ;
hence rng f c= rng g by A2; :: 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; :: thesis: verum