let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),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 X be Subset of (CQC-WFF Al); :: thesis: for f, g being FinSequence of [:(CQC-WFF Al),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 Al),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;

hence f ^ g <> {} ; :: according to CQC_THE1:def 5 :: thesis: for n being Nat st 1 <= n & n <= len (f ^ g) holds

f ^ g,n is_a_correct_step_wrt X

let n be Nat; :: thesis: ( 1 <= n & n <= len (f ^ g) implies f ^ g,n is_a_correct_step_wrt X )

assume that

A3: 1 <= n and

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

for f, g being FinSequence of [:(CQC-WFF Al),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 X be Subset of (CQC-WFF Al); :: thesis: for f, g being FinSequence of [:(CQC-WFF Al),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 Al),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;

hence f ^ g <> {} ; :: according to CQC_THE1:def 5 :: thesis: for n being Nat st 1 <= n & n <= len (f ^ g) holds

f ^ g,n is_a_correct_step_wrt X

let n be Nat; :: thesis: ( 1 <= n & n <= len (f ^ g) implies f ^ g,n is_a_correct_step_wrt X )

assume that

A3: 1 <= n and

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

now :: thesis: f ^ g,n is_a_correct_step_wrt Xend;

hence
f ^ g,n is_a_correct_step_wrt X
; :: thesis: verumper cases
( n <= len f or len f < n )
;

end;

suppose A5:
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;

hence f ^ g,n is_a_correct_step_wrt X by A3, A5, Th23; :: thesis: verum

end;hence f ^ g,n is_a_correct_step_wrt X by A3, A5, Th23; :: thesis: verum

suppose A6:
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;

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 X ) by A2, A8;

hence f ^ g,n is_a_correct_step_wrt X by A8, A9, Th24; :: thesis: verum

end;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 X ) by A2, A8;

hence f ^ g,n is_a_correct_step_wrt X by A8, A9, Th24; :: thesis: verum