A16: k < len (Rev F) by A14, NAT_1:13;
then 0 + k < len F by FINSEQ_5:def 3;
then A17: (0 + k) + (- k) < (len F) + (- k) by XREAL_1:8;
then reconsider i = (len F) - k as Element of NAT by INT_1:3;
A18: (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 ;
A19: 0 + 1 <= i by A17, NAT_1:13;
then A20: 1 <= i + 1 by NAT_1:13;
assume A21: k <> 0 ; :: thesis: ex q1, p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )
then A22: 0 + 1 <= k by NAT_1:13;
then consider pk being Element of CQC-WFF Al such that
A23: pk = (Rev F) . k and
A24: |- (f ^ <*p*>) ^ <*pk*> by A12, A14, NAT_1:13;
len F < (len F) + k by A21, XREAL_1:29;
then A25: (len F) + (- k) < ((len F) + k) + (- k) by XREAL_1:8;
then consider p1, q1 being Element of CQC-WFF Al such that
A26: p1 = (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) . (i + 1) and
A27: q1 = F . i and
A28: F . (i + 1) = p1 => q1 by A6, A8, A19;
set g1 = (f ^ <*p*>) ^ <*p1*>;
A29: Suc ((f ^ <*p*>) ^ <*p1*>) = p1 by CALCUL_1:5;
len ((f ^ (IdFinS (p,n))) ^ <*q*>) < (len ((f ^ (IdFinS (p,n))) ^ <*q*>)) + i by A17, XREAL_1:29;
then (len ((f ^ (IdFinS (p,n))) ^ <*q*>)) + (- i) < ((len ((f ^ (IdFinS (p,n))) ^ <*q*>)) + i) + (- i) by XREAL_1:8;
then k < (len (f ^ (IdFinS (p,n)))) + (len <*q*>) by FINSEQ_1:22, A18;
then k < (len (f ^ (IdFinS (p,n)))) + 1 by FINSEQ_1:39;
then k <= len (f ^ (IdFinS (p,n))) by NAT_1:13;
then A30: k in dom (f ^ (IdFinS (p,n))) by A22, FINSEQ_3:25;
then A31: ((f ^ (IdFinS (p,n))) ^ <*q*>) . k = (((f ^ (IdFinS (p,n))) ^ <*q*>) | (dom (f ^ (IdFinS (p,n))))) . k by FUNCT_1:49;
A32: (f ^ (IdFinS (p,n))) . k in rng (f ^ (IdFinS (p,n))) by A30, FUNCT_1:3;
rng (f ^ (IdFinS (p,n))) = (rng f) \/ (rng (IdFinS (p,n))) by FINSEQ_1:31
.= (rng f) \/ (rng <*p*>) by A1, Th31
.= rng (f ^ <*p*>) by FINSEQ_1:31 ;
then A33: (f ^ (IdFinS (p,n))) . k in rng (Ant ((f ^ <*p*>) ^ <*p1*>)) by A32, CALCUL_1:5;
i + 1 <= len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by A6, A25, NAT_1:13;
then i + 1 in dom (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by A20, FINSEQ_3:25;
then i + 1 in dom ((f ^ (IdFinS (p,n))) ^ <*q*>) by FINSEQ_5:57;
then p1 = ((f ^ (IdFinS (p,n))) ^ <*q*>) . (((len ((f ^ (IdFinS (p,n))) ^ <*q*>)) - (i + 1)) + 1) by A26, FINSEQ_5:58
.= ((f ^ (IdFinS (p,n))) ^ <*q*>) . ((len ((f ^ (IdFinS (p,n))) ^ <*q*>)) - i) ;
then p1 = (f ^ (IdFinS (p,n))) . k by A31, FINSEQ_1:21, A18;
then ex j1 being Nat st
( j1 in dom (Ant ((f ^ <*p*>) ^ <*p1*>)) & (Ant ((f ^ <*p*>) ^ <*p1*>)) . j1 = p1 ) by A33, FINSEQ_2:10;
then Suc ((f ^ <*p*>) ^ <*p1*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p1*>) by A29, CALCUL_1:def 16;
then A34: |- (f ^ <*p*>) ^ <*p1*> by CALCUL_1:33;
take q1 = q1; :: thesis: ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )
k + 1 in dom (Rev F) by A13, A14, FINSEQ_3:25;
then ( i = ((len F) - (k + 1)) + 1 & k + 1 in dom F ) by FINSEQ_5:57;
then A35: q1 = (Rev F) . (k + 1) by A27, FINSEQ_5:58;
k in dom (Rev F) by A22, A16, FINSEQ_3:25;
then k in dom F by FINSEQ_5:57;
then pk = p1 => q1 by A23, A28, FINSEQ_5:58;
then |- (f ^ <*p*>) ^ <*q1*> by A24, A34, CALCUL_1:56;
hence ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) by A35; :: thesis: verum

len (Rev F) = len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by A6, FINSEQ_5:def 3;
then A36: 1 in dom (Rev F) by A4, FINSEQ_3:25;
then reconsider p1 = (Rev F) . 1 as Element of CQC-WFF Al by FINSEQ_2:11;
assume A37: k = 0 ; :: thesis: ex p1, p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )
take p1 = p1; :: thesis: ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )
1 in dom F by A36, FINSEQ_5:57;
then p1 = F . (((len F) - 1) + 1) by FINSEQ_5:58
.= Impl (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by A5, A6 ;
hence ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) by A10, A37; :: thesis: verum