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

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