let Al be QC-alphabet ; :: thesis:
let p be Element of CQC-WFF Al; :: thesis:
let f be FinSequence of CQC-WFF Al; :: thesis:
let P be Permutation of (dom f); :: thesis:
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 A2, A4, FINSEQ_5:def 3;
defpred S₁[ 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:
A9: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A10: S₁[k] ; :: thesis:
assume that
A11: 1 <= k + 1 and
A12: k + 1 <= len (Rev F) ; :: thesis:

A13: now :: thesis:

A14: k < len (Rev F) by A12, NAT_1:13;
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 A4, FINSEQ_5:def 3
.= k ;
then reconsider j = (len (f ^ <*p*>)) - i as Nat ;
A17: 0 + 1 <= i by A15, NAT_1:13;
then A18: 1 <= i + 1 by NAT_1:13;
assume A19: k <> 0 ; :: thesis:
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 A10, A12, NAT_1:13;
len F < (len F) + k by A19, XREAL_1:29;
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:
k + 1 in dom (Rev F) by A11, A12, FINSEQ_3:25;
then ( i = ((len F) - (k + 1)) + 1 & k + 1 in dom F ) by FINSEQ_5:57;
then A27: q1 = (Rev F) . (k + 1) by A25, FINSEQ_5:58;
len (f ^ <*p*>) < (len (f ^ <*p*>)) + i by A15, XREAL_1:29;
then (len (f ^ <*p*>)) + (- i) < ((len (f ^ <*p*>)) + i) + (- i) by XREAL_1:8;
then j < (len f) + (len <*p*>) 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 A20, A16, FINSEQ_3:25;
then A29: (f ^ <*p*>) . j = ((f ^ <*p*>) | (dom f)) . j by FUNCT_1:49;
j in rng P by A28, FUNCT_2:def 3;
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 A4, A23, NAT_1:13;
then i + 1 in dom (Rev (f ^ <*p*>)) by A18, FINSEQ_3:25;
then i + 1 in dom (f ^ <*p*>) by FINSEQ_5:57;
then p1 = (f ^ <*p*>) . (((len (f ^ <*p*>)) - (i + 1)) + 1) by A24, FINSEQ_5:58
.= (f ^ <*p*>) . ((len (f ^ <*p*>)) - i) ;
then p1 = f . (P . j1) by A29, A31, FINSEQ_1:21;
then p1 = (P * f) . j1 by A30, FUNCT_1:13;
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 A32, Th19;
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 A33, CALCUL_1:def 16;
then A34: |- (Per (f,P)) ^ <*p1*> by CALCUL_1:33;
k in dom (Rev F) by A20, A14, FINSEQ_3:25;
then k in dom F by FINSEQ_5:57;
then pk = p1 => q1 by A21, A26, FINSEQ_5:58;
then |- (Per (f,P)) ^ <*q1*> by A22, A34, CALCUL_1:56;
hence ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) by A27; :: thesis:

end;

now :: thesis:

1 <= len (Rev F) by A2, A4, FINSEQ_5:def 3;
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:
take p = p; :: thesis:
1 in dom F by A35, FINSEQ_5:57;
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 A8, A36; :: thesis:

end;

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

end;

A37: S₁[ 0 ] ;
for k being Nat holds S₁[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 A38, FINSEQ_5:def 3;
then q = Begin (Rev (f ^ <*p*>)) by A1, A5, FINSEQ_5:62, FINSEQ_5:def 3;
then q = (Rev (f ^ <*p*>)) . 1 by A2, Def3;
then q = (f ^ <*p*>) . (len (f ^ <*p*>)) by FINSEQ_5:62;
then q = (f ^ <*p*>) . ((len f) + (len <*p*>)) by FINSEQ_1:22;
then q = (f ^ <*p*>) . ((len f) + 1) by FINSEQ_1:39;
hence |- (Per (f,P)) ^ <*p*> by A39, FINSEQ_1:42; :: thesis: