let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & |- f holds

|- (Ant f) ^ <*(p . (x,y))*>

let p be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & |- f holds

|- (Ant f) ^ <*(p . (x,y))*>

let x, y be bound_QC-variable of Al; :: thesis: for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & |- f holds

|- (Ant f) ^ <*(p . (x,y))*>

let f be FinSequence of CQC-WFF Al; :: thesis: ( Suc f = All (x,p) & |- f implies |- (Ant f) ^ <*(p . (x,y))*> )

assume that

A1: Suc f = All (x,p) and

A2: |- f ; :: thesis: |- (Ant f) ^ <*(p . (x,y))*>

consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that

A3: PR is a_proof and

A4: (PR . (len PR)) `1 = f by A2;

A5: (Ant f) ^ <*(p . (x,y))*> in set_of_CQC-WFF-seq Al by Def6;

then reconsider PR1 = <*[((Ant f) ^ <*(p . (x,y))*>),8]*> as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;

1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;

then A6: 1 in dom PR1 by FINSEQ_1:38;

set PR2 = PR ^ PR1;

reconsider PR2 = PR ^ PR1 as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;

A7: PR <> {} by A3;

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 A6, FINSEQ_1:def 7;

then PR2 . (len PR2) = [((Ant f) ^ <*(p . (x,y))*>),8] by FINSEQ_1:40;

then (PR2 . (len PR2)) `1 = (Ant f) ^ <*(p . (x,y))*> ;

hence |- (Ant f) ^ <*(p . (x,y))*> by A19; :: thesis: verum

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & |- f holds

|- (Ant f) ^ <*(p . (x,y))*>

let p be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & |- f holds

|- (Ant f) ^ <*(p . (x,y))*>

let x, y be bound_QC-variable of Al; :: thesis: for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & |- f holds

|- (Ant f) ^ <*(p . (x,y))*>

let f be FinSequence of CQC-WFF Al; :: thesis: ( Suc f = All (x,p) & |- f implies |- (Ant f) ^ <*(p . (x,y))*> )

assume that

A1: Suc f = All (x,p) and

A2: |- f ; :: thesis: |- (Ant f) ^ <*(p . (x,y))*>

consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that

A3: PR is a_proof and

A4: (PR . (len PR)) `1 = f by A2;

A5: (Ant f) ^ <*(p . (x,y))*> in set_of_CQC-WFF-seq Al by Def6;

now :: thesis: for a being object st a in rng <*[((Ant f) ^ <*(p . (x,y))*>),8]*> holds

a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

then
rng <*[((Ant f) ^ <*(p . (x,y))*>),8]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
;a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

let a be object ; :: thesis: ( a in rng <*[((Ant f) ^ <*(p . (x,y))*>),8]*> implies a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] )

assume a in rng <*[((Ant f) ^ <*(p . (x,y))*>),8]*> ; :: thesis: a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

then a in {[((Ant f) ^ <*(p . (x,y))*>),8]} by FINSEQ_1:38;

then a = [((Ant f) ^ <*(p . (x,y))*>),8] by TARSKI:def 1;

hence a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by A5, CQC_THE1:21, ZFMISC_1:87; :: thesis: verum

end;assume a in rng <*[((Ant f) ^ <*(p . (x,y))*>),8]*> ; :: thesis: a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

then a in {[((Ant f) ^ <*(p . (x,y))*>),8]} by FINSEQ_1:38;

then a = [((Ant f) ^ <*(p . (x,y))*>),8] by TARSKI:def 1;

hence a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by A5, CQC_THE1:21, ZFMISC_1:87; :: thesis: verum

then reconsider PR1 = <*[((Ant f) ^ <*(p . (x,y))*>),8]*> as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;

1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;

then A6: 1 in dom PR1 by FINSEQ_1:38;

set PR2 = PR ^ PR1;

reconsider PR2 = PR ^ PR1 as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;

A7: PR <> {} by A3;

now :: thesis: for n being Nat st 1 <= n & n <= len PR2 holds

PR2,n is_a_correct_step

then A19:
PR2 is a_proof
;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;

end;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 )

( k in dom PR1 & n = (len PR) + k ) implies PR2,n is_a_correct_step )

A10:
1 <= len PR
by A7, Th6;

then len PR in dom PR by FINSEQ_3:25;

then A11: f = (PR2 . (len PR)) `1 by A4, FINSEQ_1:def 7;

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 A12, FINSEQ_1:38;

then A14: k = 1 by FINSEQ_1:2, TARSKI:def 1;

then A15: PR1 . k = [((Ant f) ^ <*(p . (x,y))*>),8] by FINSEQ_1:40;

then (PR1 . k) `1 = (Ant f) ^ <*(p . (x,y))*> ;

then A16: (PR2 . n) `1 = (Ant f) ^ <*(p . (x,y))*> by A12, A13, FINSEQ_1:def 7;

(PR1 . k) `2 = 8 by A15;

then A17: (PR2 . n) `2 = 8 by A12, A13, FINSEQ_1:def 7;

len PR < n by A13, A14, NAT_1:13;

hence PR2,n is_a_correct_step by A1, A16, A17, A10, A11, Def7; :: thesis: verum

end;then len PR in dom PR by FINSEQ_3:25;

then A11: f = (PR2 . (len PR)) `1 by A4, FINSEQ_1:def 7;

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 A12, FINSEQ_1:38;

then A14: k = 1 by FINSEQ_1:2, TARSKI:def 1;

then A15: PR1 . k = [((Ant f) ^ <*(p . (x,y))*>),8] by FINSEQ_1:40;

then (PR1 . k) `1 = (Ant f) ^ <*(p . (x,y))*> ;

then A16: (PR2 . n) `1 = (Ant f) ^ <*(p . (x,y))*> by A12, A13, FINSEQ_1:def 7;

(PR1 . k) `2 = 8 by A15;

then A17: (PR2 . n) `2 = 8 by A12, A13, FINSEQ_1:def 7;

len PR < n by A13, A14, NAT_1:13;

hence PR2,n is_a_correct_step by A1, A16, A17, A10, A11, Def7; :: thesis: verum

now :: thesis: ( n in dom PR implies PR2,n is_a_correct_step )

hence
PR2,n is_a_correct_step
by A8, A9, FINSEQ_1:25; :: thesis: verumassume
n in dom PR
; :: thesis: PR2,n is_a_correct_step

then A18: ( 1 <= n & n <= len PR ) by FINSEQ_3:25;

then PR,n is_a_correct_step by A3;

hence PR2,n is_a_correct_step by A18, Th34; :: thesis: verum

end;then A18: ( 1 <= n & n <= len PR ) by FINSEQ_3:25;

then PR,n is_a_correct_step by A3;

hence PR2,n is_a_correct_step by A18, Th34; :: thesis: verum

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 A6, FINSEQ_1:def 7;

then PR2 . (len PR2) = [((Ant f) ^ <*(p . (x,y))*>),8] by FINSEQ_1:40;

then (PR2 . (len PR2)) `1 = (Ant f) ^ <*(p . (x,y))*> ;

hence |- (Ant f) ^ <*(p . (x,y))*> by A19; :: thesis: verum