let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al
for P being Permutation of (dom f) holds dom (Per (f,P)) = dom f
let f be FinSequence of CQC-WFF Al; :: thesis: for P being Permutation of (dom f) holds dom (Per (f,P)) = dom f
let P be Permutation of (dom f); :: thesis: dom (Per (f,P)) = dom f
rng P = dom f by FUNCT_2:def 3;
then dom (P * f) = dom P by RELAT_1:27;
hence dom (Per (f,P)) = dom f by FUNCT_2:52; :: thesis: verum