let X be Subset of CQC-WFF ; :: thesis: for f, g being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X & g is_a_proof_wrt X holds
f ^ g is_a_proof_wrt X
let f, g be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :]; :: thesis: ( f is_a_proof_wrt X & g is_a_proof_wrt X implies f ^ g is_a_proof_wrt X )
assume that
A1: f is_a_proof_wrt X and
A2: g is_a_proof_wrt X ; :: thesis: f ^ g is_a_proof_wrt X
f <> {} by A1, Def5;
hence f ^ g <> {} ; :: according to CQC_THE1:def 5 :: thesis: for n being Element of NAT st 1 <= n & n <= len (f ^ g) holds
f ^ g,n is_a_correct_step_wrt X
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len (f ^ g) implies f ^ g,n is_a_correct_step_wrt X )
assume A3: ( 1 <= n & n <= len (f ^ g) ) ; :: thesis: f ^ g,n is_a_correct_step_wrt X

now

per cases ( n <= len f or len f < n ) ;

suppose A4: n <= len f ; :: thesis: f ^ g,n is_a_correct_step_wrt X

then f,n is_a_correct_step_wrt X by A1, A3, Def5;
hence f ^ g,n is_a_correct_step_wrt X by A3, A4, Th60; :: thesis: verum

end;

suppose A5: len f < n ; :: thesis: f ^ g,n is_a_correct_step_wrt X

then reconsider k = n - (len f) as Element of NAT by NAT_1:21;
A6: k + (len f) = n ;
( k + (len f) <= (len g) + (len f) & (len f) + 1 <= k + (len f) ) by A3, A5, FINSEQ_1:35, NAT_1:13;
then A7: ( 1 <= k & k <= len g ) by XREAL_1:8;
then g,k is_a_correct_step_wrt X by A2, Def5;
hence f ^ g,n is_a_correct_step_wrt X by A6, A7, Th61; :: thesis: verum

end;

end;

end;

hence f ^ g,n is_a_correct_step_wrt X ; :: thesis: verum