let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al holds Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f)
let f, g be FinSequence of CQC-WFF Al; :: 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