let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al st Ant f is_Subsequence_of Ant g & Suc f = Suc g & |- f holds
|- g

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