let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al st 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & |- f & |- g holds
|- (Ant (Ant f)) ^ <*(Suc f)*>

let f, g be FinSequence of CQC-WFF Al; :: thesis: ( 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & |- f & |- g implies |- (Ant (Ant f)) ^ <*(Suc f)*> )
assume that
A1: ( 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g ) and
A2: |- f and
A3: |- g ; :: thesis: |- (Ant (Ant f)) ^ <*(Suc f)*>
consider PR1 being FinSequence of such that
A4: PR1 is a_proof and
A5: g = (PR1 . (len PR1)) `1 by A3;
consider PR being FinSequence of such that
A6: PR is a_proof and
A7: f = (PR . (len PR)) `1 by A2;
A8: (Ant (Ant f)) ^ <*(Suc f)*> in set_of_CQC-WFF-seq Al by Def6;
now :: thesis: for a being object st a in rng <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> holds
a in
let a be object ; :: thesis: ( a in rng <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> implies a in )
assume a in rng <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> ; :: thesis:
then a in {[((Ant (Ant f)) ^ <*(Suc f)*>),3]} by FINSEQ_1:38;
then a = [((Ant (Ant f)) ^ <*(Suc f)*>),3] by TARSKI:def 1;
hence a in by ; :: thesis: verum
end;
then rng <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> c= ;
then reconsider PR2 = <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> as FinSequence of by FINSEQ_1:def 4;
1 in Seg 1 by ;
then A9: 1 in dom PR2 by FINSEQ_1:38;
set PR3 = (PR ^ PR1) ^ PR2;
reconsider PR3 = (PR ^ PR1) ^ PR2 as FinSequence of ;
A10: PR <> {} by A6;
now :: thesis: for n being Nat st 1 <= n & n <= len PR3 holds
PR3,n is_a_correct_step
let n be Nat; :: thesis: ( 1 <= n & n <= len PR3 implies PR3,n is_a_correct_step )
assume ( 1 <= n & n <= len PR3 ) ; :: thesis: PR3,n is_a_correct_step
then A11: n in dom PR3 by FINSEQ_3:25;
A12: now :: thesis: ( ex k being Nat st
( k in dom PR2 & n = (len (PR ^ PR1)) + k ) implies PR3,n is_a_correct_step )
given k being Nat such that A13: k in dom PR2 and
A14: n = (len (PR ^ PR1)) + k ; :: thesis: PR3,n is_a_correct_step
k in Seg 1 by ;
then A15: k = 1 by ;
then A16: PR2 . k = [((Ant (Ant f)) ^ <*(Suc f)*>),3] by FINSEQ_1:40;
then (PR2 . k) `1 = (Ant (Ant f)) ^ <*(Suc f)*> ;
then A17: (PR3 . n) `1 = (Ant (Ant f)) ^ <*(Suc f)*> by ;
(PR2 . k) `2 = 3 by A16;
then A18: (PR3 . n) `2 = 3 by ;
A19: len (PR ^ PR1) < n by ;
A20: 1 <= len PR by ;
then len PR in dom PR by FINSEQ_3:25;
then A21: f = ((PR ^ PR1) . (len PR)) `1 by ;
A22: PR1 <> {} by A4;
then A23: len PR < len (PR ^ PR1) by Th6;
then len PR in dom (PR ^ PR1) by ;
then A24: f = (PR3 . (len PR)) `1 by ;
1 <= len PR1 by ;
then len PR1 in dom PR1 by FINSEQ_3:25;
then g = ((PR ^ PR1) . ((len PR) + (len PR1))) `1 by ;
then A25: g = ((PR ^ PR1) . (len (PR ^ PR1))) `1 by FINSEQ_1:22;
1 <= len (PR ^ PR1) by ;
then len (PR ^ PR1) in dom (PR ^ PR1) by FINSEQ_3:25;
then A26: g = (PR3 . (len (PR ^ PR1))) `1 by ;
1 <= len (PR ^ PR1) by ;
hence PR3,n is_a_correct_step by A1, A17, A18, A20, A23, A24, A19, A26, Def7; :: thesis: verum
end;
now :: thesis: ( n in dom (PR ^ PR1) implies PR3,n is_a_correct_step )
A27: now :: thesis: ( ex k being Nat st
( k in dom PR1 & n = (len PR) + k ) implies PR3,n is_a_correct_step )
given k being Nat such that A28: k in dom PR1 and
A29: n = (len PR) + k ; :: thesis: PR3,n is_a_correct_step
A30: 1 <= k by ;
A31: k <= len PR1 by ;
then n <= (len PR1) + (len PR) by ;
then A32: n <= len (PR ^ PR1) by FINSEQ_1:22;
k <= n by ;
then A33: 1 <= n by ;
PR1,k is_a_correct_step by A4, A30, A31;
then PR ^ PR1,n is_a_correct_step by ;
hence PR3,n is_a_correct_step by ; :: thesis: verum
end;
assume n in dom (PR ^ PR1) ; :: thesis: PR3,n is_a_correct_step
hence PR3,n is_a_correct_step by ; :: thesis: verum
end;
hence PR3,n is_a_correct_step by ; :: thesis: verum
end;
then A39: PR3 is a_proof ;
PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + (len PR2)) by FINSEQ_1:22;
then PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + 1) by FINSEQ_1:39;
then PR3 . (len PR3) = PR2 . 1 by ;
then PR3 . (len PR3) = [((Ant (Ant f)) ^ <*(Suc f)*>),3] by FINSEQ_1:40;
then (PR3 . (len PR3)) `1 = (Ant (Ant f)) ^ <*(Suc f)*> ;
hence |- (Ant (Ant f)) ^ <*(Suc f)*> by A39; :: thesis: verum