let f, g be FinSequence of CQC-WFF ; :: 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 A2: i in dom (Seq ((g ^ f) | (seq (len g),(len f)))) ; :: thesis: (Seq ((g ^ f) | (seq (len g),(len f)))) . i = f . i
A3: (Seq ((g ^ f) | (seq (len g),(len f)))) . i = ((Sgm (seq (len g),(len f))) * (g ^ f)) . i by Th16;
A4: i in dom f by A2, Th17;
then A5: i in dom (Sgm (seq (len g),(len f))) by Th11;
then (Seq ((g ^ f) | (seq (len g),(len f)))) . i = (g ^ f) . ((Sgm (seq (len g),(len f))) . i) by A3, FUNCT_1:23;
then (Seq ((g ^ f) | (seq (len g),(len f)))) . i = (g ^ f) . ((len g) + i) by A5, Th13;
hence (Seq ((g ^ f) | (seq (len g),(len f)))) . i = f . i by A4, 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:17;
hence f is_Subsequence_of g ^ f by CALCUL_1:def 4; :: thesis: verum