let p be Element of CQC-WFF ; :: thesis: for f being FinSequence of CQC-WFF
for P being Permutation of (dom f) st |- f ^ <*p*> holds
|- (Per f,P) ^ <*p*>
let f be FinSequence of CQC-WFF ; :: 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:45;
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