let B be set ; :: thesis:
let R be Rule; :: thesis:
let P1, P2 be Formula-sequence; :: thesis:
assume that
A1: P1 is B,R -correct and
A2: P2 is B,R -correct ; :: thesis:
let k be Nat; :: according to PROOFS_1:def 7 :: 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 B,R by A1;
then P1 ^ (<*> {}),k is_a_correct_step_wrt B,R by FINSEQ_1:34;
hence P1 ^ P2,k is_a_correct_step_wrt B,R by A5, Lm41; :: thesis:

end;

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

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

end;

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

consider j being Nat such that
A12: j in dom P2 and
A13: k = (len P1) + j by A3, A10, FINSEQ_1:25;
A15: P2,j is_a_correct_step_wrt B,R by A2, A12;
A16: (P1 ^ P2) . k = P2 . j by A12, A13, FINSEQ_1:def 7;
then consider Q being Formula-finset such that
A20: [Q,(P2 . j)] in R and
A21: for t being object st t in Q holds
ex i being Nat st
( i in dom P2 & i < j & P2 . i = t ) by A11, A15;
for t being object st t in Q holds
ex u being Nat st
( u in dom (P1 ^ P2) & u < k & (P1 ^ P2) . u = t )

proof

let t be object ; :: thesis:
assume t in Q ; :: thesis:
then consider i being Nat such that
A25: i in dom P2 and
A26: i < j and
A27: P2 . i = t by A21;
take u = (len P1) + i; :: thesis:
A30: ( 1 <= i & i <= len P2 ) by A25, FINSEQ_3:25;
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 = t by A27, A30, FINSEQ_1:65; :: thesis:

end;

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

end;

end;