let g, f be FinSequence of CQC-WFF ; :: thesis: Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f)
reconsider gf = (g ^ f) | (seq ((len g),(len f))) as FinSubsequence ;
Seq gf = gf * (Sgm (dom gf)) by FINSEQ_1:def 14
.= gf * (Sgm (seq ((len g),(len f)))) by Th15
.= ((g ^ f) | (rng (Sgm (seq ((len g),(len f)))))) * (Sgm (seq ((len g),(len f)))) by Th12
.= (g ^ f) * (Sgm (seq ((len g),(len f)))) by FUNCT_4:2 ;
hence Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f) ; :: thesis: verum