let A be non empty Subset of GRZ-formula-set; :: thesis:
let R be GRZ-rule; :: thesis:
let P1, P2 be GRZ-formula-sequence; :: thesis:
set P0 = <*> GRZ-formula-set;
assume that
A1: P1 is A,R -correct and
A2: P2 is A,R -correct ; :: thesis:
let k be Element of NAT ; :: according to GRZLOG_1:def 30 :: thesis:
assume A3: k in dom (P1 ^ P2) ; :: thesis:

per cases ;

suppose A5: k in dom P1 ; :: thesis:

then P1,k is_a_correct_step_wrt A,R by A1;
then P1 ^ (<*> GRZ-formula-set),k is_a_correct_step_wrt A,R by FINSEQ_1:34;
hence P1 ^ P2,k is_a_correct_step_wrt A,R by A5, Lm41; :: thesis:

end;

suppose (P1 ^ P2) . k in A ; :: thesis:

hence P1 ^ P2,k is_a_correct_step_wrt A,R ; :: thesis:

end;

suppose that A10: not k in dom P1 and
A11: not (P1 ^ P2) . k in A ; :: thesis:

consider j being Nat such that
A12: j in dom P2 and
A13: k = (len P1) + j by A3, A10, FINSEQ_1:25;
reconsider m = j as Element of NAT by ORDINAL1:def 12;
A15: P2,m is_a_correct_step_wrt A,R by A2, A12;
A16: (P1 ^ P2) . k = P2 . m by A12, A13, FINSEQ_1:def 7;
then consider Q being GRZ-formula-finset such that
A20: [Q,(P2 . m)] in R and
A21: for q being FinSequence st q in Q holds
ex i being Element of NAT st
( i in dom P2 & i < m & P2 . i = q ) by A11, A15;
for q being FinSequence st q in Q holds
ex u being Element of NAT st
( u in dom (P1 ^ P2) & u < k & (P1 ^ P2) . u = q )

proof

let q be FinSequence; :: thesis:
assume q in Q ; :: thesis:
then consider i being Element of NAT such that
A25: i in dom P2 and
A26: i < m and
A27: P2 . i = q by A21;
reconsider j = i as Nat ;
reconsider u = (len P1) + i as Element of NAT by ORDINAL1:def 12;
take u ; :: thesis:
j in Seg (len P2) by A25, FINSEQ_1:def 3;
then A30: ( 1 <= j & j <= len P2 ) by FINSEQ_1:1;
thus u in dom (P1 ^ P2) by A25, FINSEQ_1:28; :: thesis:
thus u < k by A13, A26, XREAL_1:6; :: thesis:
thus (P1 ^ P2) . u = q by A27, A30, FINSEQ_1:65; :: thesis:

end;

hence P1 ^ P2,k is_a_correct_step_wrt A,R by A16, A20; :: thesis:

end;

end;