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;

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

( 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)

then
rng f c= rng (g | N)
;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 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

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