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 |- (Per (f,P)) ^ <*(Impl (Rev (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 |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> holds
|- (Per (f,P)) ^ <*p*>

let f be FinSequence of CQC-WFF Al; :: thesis: for P being Permutation of (dom f) st |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> holds
|- (Per (f,P)) ^ <*p*>

let P be Permutation of (dom f); :: thesis: ( |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> implies |- (Per (f,P)) ^ <*p*> )
set g = f ^ <*p*>;
set h = Rev (f ^ <*p*>);
A1: 1 <= len (f ^ <*p*>) by CALCUL_1:10;
then A2: 1 <= len (Rev (f ^ <*p*>)) by FINSEQ_5:def 3;
then consider F being FinSequence of CQC-WFF Al such that
A3: Impl (Rev (f ^ <*p*>)) = F . (len (Rev (f ^ <*p*>))) and
A4: len F = len (Rev (f ^ <*p*>)) and
A5: ( F . 1 = Begin (Rev (f ^ <*p*>)) or len (Rev (f ^ <*p*>)) = 0 ) and
A6: for n being Nat st 1 <= n & n < len (Rev (f ^ <*p*>)) holds
ex p, q being Element of CQC-WFF Al st
( p = (Rev (f ^ <*p*>)) . (n + 1) & q = F . n & F . (n + 1) = p => q ) by Def4;
set H = Rev F;
A7: 1 <= len (Rev F) by ;
defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len (Rev F) implies ex p being Element of CQC-WFF Al st
( p = (Rev F) . \$1 & |- (Per (f,P)) ^ <*p*> ) );
assume A8: |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> ; :: thesis: |- (Per (f,P)) ^ <*p*>
A9: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A10: S1[k] ; :: thesis: S1[k + 1]
assume that
A11: 1 <= k + 1 and
A12: k + 1 <= len (Rev F) ; :: thesis: ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

A13: now :: thesis: ( k <> 0 implies ex q1, p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) )
A14: k < len (Rev F) by ;
then 0 + k < len F by FINSEQ_5:def 3;
then A15: (0 + k) + (- k) < (len F) + (- k) by XREAL_1:8;
then reconsider i = (len F) - k as Element of NAT by INT_1:3;
A16: (len (f ^ <*p*>)) - i = (len (f ^ <*p*>)) - ((len (f ^ <*p*>)) - k) by
.= k ;
then reconsider j = (len (f ^ <*p*>)) - i as Nat ;
A17: 0 + 1 <= i by ;
then A18: 1 <= i + 1 by NAT_1:13;
assume A19: k <> 0 ; :: thesis: ex q1, p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

then A20: 0 + 1 <= k by NAT_1:13;
then consider pk being Element of CQC-WFF Al such that
A21: pk = (Rev F) . k and
A22: |- (Per (f,P)) ^ <*pk*> by ;
len F < (len F) + k by ;
then A23: (len F) + (- k) < ((len F) + k) + (- k) by XREAL_1:8;
then consider p1, q1 being Element of CQC-WFF Al such that
A24: p1 = (Rev (f ^ <*p*>)) . (i + 1) and
A25: q1 = F . i and
A26: F . (i + 1) = p1 => q1 by A4, A6, A17;
take q1 = q1; :: thesis: ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

k + 1 in dom (Rev F) by ;
then ( i = ((len F) - (k + 1)) + 1 & k + 1 in dom F ) by FINSEQ_5:57;
then A27: q1 = (Rev F) . (k + 1) by ;
len (f ^ <*p*>) < (len (f ^ <*p*>)) + i by ;
then (len (f ^ <*p*>)) + (- i) < ((len (f ^ <*p*>)) + i) + (- i) by XREAL_1:8;
then j < (len f) + () by FINSEQ_1:22;
then j < (len f) + 1 by FINSEQ_1:39;
then j <= len f by NAT_1:13;
then A28: j in dom f by ;
then A29: (f ^ <*p*>) . j = ((f ^ <*p*>) | (dom f)) . j by FUNCT_1:49;
j in rng P by ;
then consider a being object such that
A30: a in dom P and
A31: P . a = j by FUNCT_1:def 3;
A32: a in dom f by A30;
then reconsider j1 = a as Element of NAT ;
set g1 = (Per (f,P)) ^ <*p1*>;
i + 1 <= len (Rev (f ^ <*p*>)) by ;
then i + 1 in dom (Rev (f ^ <*p*>)) by ;
then i + 1 in dom (f ^ <*p*>) by FINSEQ_5:57;
then p1 = (f ^ <*p*>) . (((len (f ^ <*p*>)) - (i + 1)) + 1) by
.= (f ^ <*p*>) . ((len (f ^ <*p*>)) - i) ;
then p1 = f . (P . j1) by ;
then p1 = (P * f) . j1 by ;
then Suc ((Per (f,P)) ^ <*p1*>) = (Per (f,P)) . j1 by CALCUL_1:5;
then A33: Suc ((Per (f,P)) ^ <*p1*>) = (Ant ((Per (f,P)) ^ <*p1*>)) . j1 by CALCUL_1:5;
j1 in dom (Per (f,P)) by ;
then j1 in dom (Ant ((Per (f,P)) ^ <*p1*>)) by CALCUL_1:5;
then Suc ((Per (f,P)) ^ <*p1*>) is_tail_of Ant ((Per (f,P)) ^ <*p1*>) by ;
then A34: |- (Per (f,P)) ^ <*p1*> by CALCUL_1:33;
k in dom (Rev F) by ;
then k in dom F by FINSEQ_5:57;
then pk = p1 => q1 by ;
then |- (Per (f,P)) ^ <*q1*> by ;
hence ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) by A27; :: thesis: verum
end;
now :: thesis: ( k = 0 implies ex p, p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) )
1 <= len (Rev F) by ;
then A35: 1 in dom (Rev F) by FINSEQ_3:25;
then reconsider p = (Rev F) . 1 as Element of CQC-WFF Al by FINSEQ_2:11;
assume A36: k = 0 ; :: thesis: ex p, p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

take p = p; :: thesis: ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

1 in dom F by ;
then p = F . (((len F) - 1) + 1) by FINSEQ_5:58
.= Impl (Rev (f ^ <*p*>)) by A3, A4 ;
hence ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) by ; :: thesis: verum
end;
hence ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) by A13; :: thesis: verum
end;
A37: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A37, A9);
then consider q being Element of CQC-WFF Al such that
A38: q = (Rev F) . (len (Rev F)) and
A39: |- (Per (f,P)) ^ <*q*> by A7;
q = (Rev F) . (len F) by ;
then q = Begin (Rev (f ^ <*p*>)) by ;
then q = (Rev (f ^ <*p*>)) . 1 by ;
then q = (f ^ <*p*>) . (len (f ^ <*p*>)) by FINSEQ_5:62;
then q = (f ^ <*p*>) . ((len f) + ()) by FINSEQ_1:22;
then q = (f ^ <*p*>) . ((len f) + 1) by FINSEQ_1:39;
hence |- (Per (f,P)) ^ <*p*> by ; :: thesis: verum