let X be Subset of CQC-WFF ; 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 :]; ( 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
; f ^ g is_a_proof_wrt X
A3:
f <> {}
by A1, Def5;
thus
f ^ g <> {}
by A3; CQC_THE1:def 5 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 ; ( 1 <= n & n <= len (f ^ g) implies f ^ g,n is_a_correct_step_wrt X )
assume that
A4:
1 <= n
and
A5:
n <= len (f ^ g)
; f ^ g,n is_a_correct_step_wrt X
A6:
now per cases
( n <= len f or len f < n )
;
suppose A9:
len f < n
;
f ^ g,n is_a_correct_step_wrt Xreconsider k =
n - (len f) as
Element of
NAT by A9, NAT_1:21;
A10:
k + (len f) <= (len g) + (len f)
by A5, FINSEQ_1:35;
A11:
(len f) + 1
<= k + (len f)
by A9, NAT_1:13;
A12:
1
<= k
by A11, XREAL_1:8;
A13:
k <= len g
by A10, XREAL_1:8;
A14:
(
k + (len f) = n &
g,
k is_a_correct_step_wrt X )
by A2, A12, A13, Def5;
thus
f ^ g,
n is_a_correct_step_wrt X
by A12, A13, A14, Th61;
verum end;
thus
f ^ g,n is_a_correct_step_wrt X
by A6; verum