let Al be QC-alphabet ; 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; 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)
; verum