let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al
for n being Element of NAT
for f being FinSequence of CQC-WFF Al st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>

let p, q be Element of CQC-WFF Al; :: thesis: for n being Element of NAT
for f being FinSequence of CQC-WFF Al st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>

let n be Element of NAT ; :: thesis: for f being FinSequence of CQC-WFF Al st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>

let f be FinSequence of CQC-WFF Al; :: thesis: ( 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> implies |- (f ^ <*p*>) ^ <*q*> )
assume that
A1: 1 <= n and
A2: |- (f ^ (IdFinS (p,n))) ^ <*q*> ; :: thesis: |- (f ^ <*p*>) ^ <*q*>
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: 1 <= len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by FINSEQ_5:def 3;
then consider F being FinSequence of CQC-WFF Al such that
A5: Impl (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) = F . (len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>))) and
A6: len F = len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) and
A7: ( F . 1 = Begin (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) or len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) = 0 ) and
A8: for n being Nat st 1 <= n & n < len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) holds
ex p, q being Element of CQC-WFF Al st
( p = (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) . (n + 1) & q = F . n & F . (n + 1) = p => q ) by Def4;
set H = Rev F;
A9: 1 <= len (Rev F) by ;
defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len (Rev F) implies ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . \$1 & |- (f ^ <*p*>) ^ <*p1*> ) );
|- ((f ^ <*p*>) ^ (f ^ (IdFinS (p,n)))) ^ <*q*> by ;
then |- (f ^ <*p*>) ^ ((f ^ (IdFinS (p,n))) ^ <*q*>) by FINSEQ_1:32;
then A10: |- (f ^ <*p*>) ^ <*(Impl (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)))*> by ;
A11: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A12: S1[k] ; :: thesis: S1[k + 1]
assume that
A13: 1 <= k + 1 and
A14: k + 1 <= len (Rev F) ; :: thesis: ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )

A15: now :: thesis: ( k <> 0 implies ex q1, p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) )
A16: k < len (Rev F) by ;
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
.= k ;
A19: 0 + 1 <= i by ;
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 ;
len F < (len F) + k by ;
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 ;
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)))) + () by ;
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 ;
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 ;
rng (f ^ (IdFinS (p,n))) = (rng f) \/ (rng (IdFinS (p,n))) by FINSEQ_1:31
.= (rng f) \/ () by
.= rng (f ^ <*p*>) by FINSEQ_1:31 ;
then A33: (f ^ (IdFinS (p,n))) . k in rng (Ant ((f ^ <*p*>) ^ <*p1*>)) by ;
i + 1 <= len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by ;
then i + 1 in dom (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by ;
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
.= ((f ^ (IdFinS (p,n))) ^ <*q*>) . ((len ((f ^ (IdFinS (p,n))) ^ <*q*>)) - i) ;
then p1 = (f ^ (IdFinS (p,n))) . k by ;
then ex j1 being Nat st
( j1 in dom (Ant ((f ^ <*p*>) ^ <*p1*>)) & (Ant ((f ^ <*p*>) ^ <*p1*>)) . j1 = p1 ) by ;
then Suc ((f ^ <*p*>) ^ <*p1*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p1*>) by ;
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 ;
then ( i = ((len F) - (k + 1)) + 1 & k + 1 in dom F ) by FINSEQ_5:57;
then A35: q1 = (Rev F) . (k + 1) by ;
k in dom (Rev F) by ;
then k in dom F by FINSEQ_5:57;
then pk = p1 => q1 by ;
then |- (f ^ <*p*>) ^ <*q1*> by ;
hence ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) by A35; :: thesis: verum
end;
now :: thesis: ( k = 0 implies ex p1, p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) )
len (Rev F) = len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by ;
then A36: 1 in dom (Rev F) by ;
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 ;
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 ; :: thesis: verum
end;
hence ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) by A15; :: thesis: verum
end;
A38: S1[ 0 ] ;
for k being Nat holds S1[k] from then consider p1 being Element of CQC-WFF Al such that
A39: p1 = (Rev F) . (len (Rev F)) and
A40: |- (f ^ <*p*>) ^ <*p1*> by A9;
p1 = (Rev F) . (len F) by ;
then p1 = Begin (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by ;
then p1 = (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) . 1 by ;
then p1 = ((f ^ (IdFinS (p,n))) ^ <*q*>) . (len ((f ^ (IdFinS (p,n))) ^ <*q*>)) by FINSEQ_5:62;
then p1 = ((f ^ (IdFinS (p,n))) ^ <*q*>) . ((len (f ^ (IdFinS (p,n)))) + ()) by FINSEQ_1:22;
then p1 = ((f ^ (IdFinS (p,n))) ^ <*q*>) . ((len (f ^ (IdFinS (p,n)))) + 1) by FINSEQ_1:39;
hence |- (f ^ <*p*>) ^ <*q*> by ; :: thesis: verum