let Al be QC-alphabet ; for f, g being FinSequence of CQC-WFF Al holds dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f
let f, g be FinSequence of CQC-WFF Al; dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f
rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f))
by Th12;
then A1:
rng (Sgm (seq ((len g),(len f)))) c= dom (g ^ f)
by Th14;
dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom ((Sgm (seq ((len g),(len f)))) * (g ^ f))
by Th16;
then
dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom (Sgm (seq ((len g),(len f))))
by A1, RELAT_1:27;
hence
dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f
by Th11; verum