let p, q be Element of CQC-WFF ; :: thesis:
let n be Element of NAT ; :: thesis:
let f be FinSequence of CQC-WFF ; :: thesis:
assume A1: ( 1 <= n & |- (f ^ (IdFinS p,n)) ^ <*q*> ) ; :: thesis:
then |- ((f ^ <*p*>) ^ (f ^ (IdFinS p,n))) ^ <*q*> by Th20;
then A2: |- (f ^ <*p*>) ^ ((f ^ (IdFinS p,n)) ^ <*q*>) by FINSEQ_1:45;
set g = (f ^ (IdFinS p,n)) ^ <*q*>;
set h = Rev ((f ^ (IdFinS p,n)) ^ <*q*>);
A3: 1 <= len ((f ^ (IdFinS p,n)) ^ <*q*>) by CALCUL_1:10;
then A4: |- (f ^ <*p*>) ^ <*(Impl (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)))*> by A2, Th28;
A5: 1 <= len (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) by A3, FINSEQ_5:def 3;
then consider F being FinSequence of CQC-WFF such that
A6: ( Impl (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) = F . (len (Rev ((f ^ (IdFinS p,n)) ^ <*q*>))) & len F = len (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) & ( F . 1 = Begin (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) or len (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) = 0 ) & ( for n being Element of NAT st 1 <= n & n < len (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) holds
ex p, q being Element of CQC-WFF st
( p = (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) by Def4;
set H = Rev F;
defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 <= len (Rev F) implies ex p1 being Element of CQC-WFF st
( p1 = (Rev F) . $1 & |- (f ^ <*p*>) ^ <*p1*> ) );
A7: S₁[ 0 ] ;
A8: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A9: S₁[k] ; :: thesis:
assume A10: ( 1 <= k + 1 & k + 1 <= len (Rev F) ) ; :: thesis:

A11: now

assume A12: k = 0 ; :: thesis:
len (Rev F) = len (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) by A6, FINSEQ_5:def 3;
then A13: 1 in dom (Rev F) by A5, FINSEQ_3:27;
then reconsider p1 = (Rev F) . 1 as Element of CQC-WFF by FINSEQ_2:13;
take p1 = p1; :: thesis:
1 in dom F by A13, FINSEQ_5:60;
then p1 = F . (((len F) - 1) + 1) by FINSEQ_5:61
.= Impl (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) by A6 ;
hence ex p1 being Element of CQC-WFF st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) by A4, A12; :: thesis:

end;

now

assume k <> 0 ; :: thesis:
then A14: ( 0 < k & k <= k + 1 ) by NAT_1:13;
then A15: ( 0 + 1 <= k & k < len (Rev F) ) by A10, NAT_1:13;
then consider pk being Element of CQC-WFF such that
A16: ( pk = (Rev F) . k & |- (f ^ <*p*>) ^ <*pk*> ) by A9;
k in dom (Rev F) by A15, FINSEQ_3:27;
then A17: k in dom F by FINSEQ_5:60;
0 + k < len F by A15, FINSEQ_5:def 3;
then A18: (0 + k) + (- k) < (len F) + (- k) by XREAL_1:10;
then reconsider i = (len F) - k as Element of NAT by INT_1:16;
A19: 0 + 1 <= i by A18, NAT_1:13;
len F < (len F) + k by A14, XREAL_1:31;
then A20: (len F) + (- k) < ((len F) + k) + (- k) by XREAL_1:10;
then consider p1, q1 being Element of CQC-WFF such that
A21: ( p1 = (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) . (i + 1) & q1 = F . i & F . (i + 1) = p1 => q1 ) by A6, A19;
A22: pk = p1 => q1 by A16, A17, A21, FINSEQ_5:61;
( 1 <= i + 1 & i + 1 <= len (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) ) by A6, A19, A20, NAT_1:13;
then i + 1 in dom (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) by FINSEQ_3:27;
then i + 1 in dom ((f ^ (IdFinS p,n)) ^ <*q*>) by FINSEQ_5:60;
then A23: p1 = ((f ^ (IdFinS p,n)) ^ <*q*>) . (((len ((f ^ (IdFinS p,n)) ^ <*q*>)) - (i + 1)) + 1) by A21, FINSEQ_5:61
.= ((f ^ (IdFinS p,n)) ^ <*q*>) . ((len ((f ^ (IdFinS p,n)) ^ <*q*>)) - i) ;
A24: (len ((f ^ (IdFinS p,n)) ^ <*q*>)) - i = (len ((f ^ (IdFinS p,n)) ^ <*q*>)) - ((len ((f ^ (IdFinS p,n)) ^ <*q*>)) - k) by A6, FINSEQ_5:def 3
.= k ;
then reconsider j = (len ((f ^ (IdFinS p,n)) ^ <*q*>)) - i as Element of NAT ;
set g1 = (f ^ <*p*>) ^ <*p1*>;
len ((f ^ (IdFinS p,n)) ^ <*q*>) < (len ((f ^ (IdFinS p,n)) ^ <*q*>)) + i by A18, XREAL_1:31;
then (len ((f ^ (IdFinS p,n)) ^ <*q*>)) + (- i) < ((len ((f ^ (IdFinS p,n)) ^ <*q*>)) + i) + (- i) by XREAL_1:10;
then j < (len (f ^ (IdFinS p,n))) + (len <*q*>) by FINSEQ_1:35;
then j < (len (f ^ (IdFinS p,n))) + 1 by FINSEQ_1:56;
then j <= len (f ^ (IdFinS p,n)) by NAT_1:13;
then A25: j in dom (f ^ (IdFinS p,n)) by A15, A24, FINSEQ_3:27;
then ((f ^ (IdFinS p,n)) ^ <*q*>) . j = (((f ^ (IdFinS p,n)) ^ <*q*>) | (dom (f ^ (IdFinS p,n)))) . j by FUNCT_1:72;
then A26: p1 = (f ^ (IdFinS p,n)) . j by A23, FINSEQ_1:33;
A27: (f ^ (IdFinS p,n)) . j in rng (f ^ (IdFinS p,n)) by A25, FUNCT_1:12;
rng (f ^ (IdFinS p,n)) = (rng f) \/ (rng (IdFinS p,n)) by FINSEQ_1:44
.= (rng f) \/ (rng <*p*>) by A1, Th31
.= rng (f ^ <*p*>) by FINSEQ_1:44 ;
then (f ^ (IdFinS p,n)) . j in rng (Ant ((f ^ <*p*>) ^ <*p1*>)) by A27, CALCUL_1:5;
then consider j1 being Nat such that
A28: ( j1 in dom (Ant ((f ^ <*p*>) ^ <*p1*>)) & (Ant ((f ^ <*p*>) ^ <*p1*>)) . j1 = p1 ) by A26, FINSEQ_2:11;
Suc ((f ^ <*p*>) ^ <*p1*>) = p1 by CALCUL_1:5;
then Suc ((f ^ <*p*>) ^ <*p1*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p1*>) by A28, CALCUL_1:def 3;
then |- (f ^ <*p*>) ^ <*p1*> by CALCUL_1:33;
then A29: |- (f ^ <*p*>) ^ <*q1*> by A16, A22, CALCUL_1:56;
A30: i = ((len F) - (k + 1)) + 1 ;
k + 1 in dom (Rev F) by A10, FINSEQ_3:27;
then k + 1 in dom F by FINSEQ_5:60;
then A31: q1 = (Rev F) . (k + 1) by A21, A30, FINSEQ_5:61;
take q1 = q1; :: thesis:
thus ex p1 being Element of CQC-WFF st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) by A29, A31; :: thesis:

end;

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

end;

A32: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A8);
1 <= len (Rev F) by A5, A6, FINSEQ_5:def 3;
then consider p1 being Element of CQC-WFF such that
A33: ( p1 = (Rev F) . (len (Rev F)) & |- (f ^ <*p*>) ^ <*p1*> ) by A32;
p1 = (Rev F) . (len F) by A33, FINSEQ_5:def 3;
then p1 = Begin (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) by A3, A6, FINSEQ_5:65, FINSEQ_5:def 3;
then p1 = (Rev ((f ^ (IdFinS p,n)) ^ <*q*>)) . 1 by A5, Def3;
then p1 = ((f ^ (IdFinS p,n)) ^ <*q*>) . (len ((f ^ (IdFinS p,n)) ^ <*q*>)) by FINSEQ_5:65;
then p1 = ((f ^ (IdFinS p,n)) ^ <*q*>) . ((len (f ^ (IdFinS p,n))) + (len <*q*>)) by FINSEQ_1:35;
then p1 = ((f ^ (IdFinS p,n)) ^ <*q*>) . ((len (f ^ (IdFinS p,n))) + 1) by FINSEQ_1:56;
hence |- (f ^ <*p*>) ^ <*q*> by A33, FINSEQ_1:59; :: thesis: