let f be FinSequence of CQC-WFF ; :: 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:46;
hence dom (Per f,P) = dom f by FUNCT_2:67; :: thesis: verum