let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al holds f is_Subsequence_of g ^ f
let f, g be FinSequence of CQC-WFF Al; :: thesis: f is_Subsequence_of g ^ f
A1: for i being Nat st i in dom (Seq ((g ^ f) | (seq ((len g),(len f))))) holds
(Seq ((g ^ f) | (seq ((len g),(len f))))) . i = f . i

proof

let i be Nat; :: thesis: ( i in dom (Seq ((g ^ f) | (seq ((len g),(len f))))) implies (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = f . i )
assume i in dom (Seq ((g ^ f) | (seq ((len g),(len f))))) ; :: thesis: (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = f . i
then A2: i in dom f by Th17;
then A3: i in dom (Sgm (seq ((len g),(len f)))) by Th11;
(Seq ((g ^ f) | (seq ((len g),(len f))))) . i = ((Sgm (seq ((len g),(len f)))) * (g ^ f)) . i by Th16;
then (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = (g ^ f) . ((Sgm (seq ((len g),(len f)))) . i) by A3, FUNCT_1:13;
then (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = (g ^ f) . ((len g) + i) by A3, Th13;
hence (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = f . i by A2, FINSEQ_1:def 7; :: thesis: verum

end;

dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f by Th17;
then Seq ((g ^ f) | (seq ((len g),(len f)))) = f by A1, FINSEQ_1:13;
hence f is_Subsequence_of g ^ f by CALCUL_1:def 4; :: thesis: verum