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

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