let Al be QC-alphabet ; :: thesis:
let p, q be Element of CQC-WFF Al; :: thesis:
let X be Subset of (CQC-WFF Al); :: thesis:
assume that
A1: p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } and
A2: p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } ; :: thesis:
ex t being Element of CQC-WFF Al st
( t = p & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = t ) ) by A1;
then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that
A3: f is_a_proof_wrt X and
A4: Effect f = p ;
ex r being Element of CQC-WFF Al st
( r = p => q & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = r ) ) by A2;
then consider g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that
A5: g is_a_proof_wrt X and
A6: Effect g = p => q ;
reconsider qq = [q,7] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th17, ZFMISC_1:87;
set h = (f ^ g) ^ <*qq*>;
A7: len ((f ^ g) ^ <*qq*>) = (len (f ^ g)) + (len <*qq*>) by FINSEQ_1:22
.= (len (f ^ g)) + 1 by FINSEQ_1:40 ;
then A8: len ((f ^ g) ^ <*qq*>) = ((len f) + (len g)) + 1 by FINSEQ_1:22;
((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>)) = qq by A7, FINSEQ_1:42;
then (((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>))) `1 = q ;
then A9: Effect ((f ^ g) ^ <*qq*>) = q by Def6;
for n being Nat st 1 <= n & n <= len ((f ^ g) ^ <*qq*>) holds
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X

proof

let n be Nat; :: thesis:
assume that
A10: 1 <= n and
A11: n <= len ((f ^ g) ^ <*qq*>) ; :: thesis:

now :: thesis:

per cases by A8, A11, NAT_1:8;

suppose n <= (len f) + (len g) ; :: thesis:

then A12: n <= len (f ^ g) by FINSEQ_1:22;
f ^ g is_a_proof_wrt X by A3, A5, Th25;
then f ^ g,n is_a_correct_step_wrt X by A10, A12;
hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X by A10, A12, Th23; :: thesis:

end;

suppose A13: n = len ((f ^ g) ^ <*qq*>) ; :: thesis:

then ((f ^ g) ^ <*qq*>) . n = qq by A7, FINSEQ_1:42;
then A14: ( (((f ^ g) ^ <*qq*>) . n) `2 = 7 & (((f ^ g) ^ <*qq*>) . n) `1 = q ) ;
len f <> 0 by A3;
then len f in Seg (len f) by FINSEQ_1:3;
then A15: len f in dom f by FINSEQ_1:def 3;
(f ^ g) ^ <*qq*> = f ^ (g ^ <*qq*>) by FINSEQ_1:32;
then A16: (((f ^ g) ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by A15, FINSEQ_1:def 7
.= p by A4, A3, Def6 ;
( dom g = Seg (len g) & len g <> 0 ) by A5, FINSEQ_1:def 3;
then A17: len g in dom g by FINSEQ_1:3;
( 1 <= len f & len f <= (len f) + (len g) ) by A3, Th21, NAT_1:11;
then (len f) + (len g) in Seg ((len f) + (len g)) by FINSEQ_1:3;
then (len f) + (len g) in Seg (len (f ^ g)) by FINSEQ_1:22;
then (len f) + (len g) in dom (f ^ g) by FINSEQ_1:def 3;
then A18: (((f ^ g) ^ <*qq*>) . ((len f) + (len g))) `1 = ((f ^ g) . ((len f) + (len g))) `1 by FINSEQ_1:def 7
.= (g . (len g)) `1 by A17, FINSEQ_1:def 7
.= p => q by A6, A5, Def6 ;
1 <= len g by A5, Th21;
then (len f) + 1 <= (len f) + (len g) by XREAL_1:7;
then A19: len f < (len f) + (len g) by NAT_1:13;
A20: ( 1 <= len f & 1 <= (len f) + (len g) ) by A3, Th21, NAT_1:12;
(len f) + (len g) < n by A8, A13, NAT_1:13;
hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X by A14, A16, A18, A19, A20, Def4; :: thesis:

end;

hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X ; :: thesis:

end;

then (f ^ g) ^ <*qq*> is_a_proof_wrt X ;
hence q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = H ) } by A9; :: thesis: