let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al
for P being Permutation of (dom f) st |- f ^ <*p*> holds
|- (Per (f,P)) ^ <*p*>
let p be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al
for P being Permutation of (dom f) st |- f ^ <*p*> holds
|- (Per (f,P)) ^ <*p*>
let f be FinSequence of CQC-WFF Al; :: thesis: for P being Permutation of (dom f) st |- f ^ <*p*> holds
|- (Per (f,P)) ^ <*p*>
let P be Permutation of (dom f); :: thesis: ( |- f ^ <*p*> implies |- (Per (f,P)) ^ <*p*> )
set g = f ^ <*p*>;
assume |- f ^ <*p*> ; :: thesis: |- (Per (f,P)) ^ <*p*>
then |- ((Per (f,P)) ^ f) ^ <*p*> by Th20;
then A1: |- (Per (f,P)) ^ (f ^ <*p*>) by FINSEQ_1:32;
1 <= len (f ^ <*p*>) by CALCUL_1:10;
then |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> by A1, Th28;
hence |- (Per (f,P)) ^ <*p*> by Th29; :: thesis: verum