let X be Subset of MC-wff; :: thesis: for f, g being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X & g is_a_proof_wrt_IPC X holds
f ^ g is_a_proof_wrt_IPC X
let f, g be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]; :: thesis: ( f is_a_proof_wrt_IPC X & g is_a_proof_wrt_IPC X implies f ^ g is_a_proof_wrt_IPC X )
assume that
A1: f is_a_proof_wrt_IPC X and
A2: g is_a_proof_wrt_IPC X ; :: thesis: f ^ g is_a_proof_wrt_IPC X
thus f ^ g <> {} by A1; :: according to INTPRO_2:def 4 :: thesis: for n being Nat st 1 <= n & n <= len (f ^ g) holds
f ^ g,n is_a_correct_step_wrt_IPC X
let n be Nat; :: thesis: ( 1 <= n & n <= len (f ^ g) implies f ^ g,n is_a_correct_step_wrt_IPC X )
assume that
A3: 1 <= n and
A4: n <= len (f ^ g) ; :: thesis: f ^ g,n is_a_correct_step_wrt_IPC X

now :: thesis: f ^ g,n is_a_correct_step_wrt_IPC X

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

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

then f,n is_a_correct_step_wrt_IPC X by A1, A3;
hence f ^ g,n is_a_correct_step_wrt_IPC X by A3, A5, Th7; :: thesis: verum

end;

suppose A6: len f < n ; :: thesis: f ^ g,n is_a_correct_step_wrt_IPC X

then reconsider k = n - (len f) as Element of NAT by NAT_1:21;
A7: k + (len f) <= (len g) + (len f) by A4, FINSEQ_1:22;
(len f) + 1 <= k + (len f) by A6, NAT_1:13;
then A8: 1 <= k by XREAL_1:6;
A9: k <= len g by A7, XREAL_1:6;
then ( k + (len f) = n & g,k is_a_correct_step_wrt_IPC X ) by A2, A8;
hence f ^ g,n is_a_correct_step_wrt_IPC X by A8, A9, Th8; :: thesis: verum

end;

end;

end;

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