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