let B be set ; :: thesis:
let R be Rule; :: thesis:
let P, P1, P2 be Formula-sequence; :: thesis:
let n be Nat; :: thesis:
assume that
A1: n in dom P and
A2: P ^ P1,n is_a_correct_step_wrt B,R ; :: thesis:
A3: P . n = (P ^ P2) . n by A1, FINSEQ_1:def 7;
P . n = (P ^ P1) . n by A1, FINSEQ_1:def 7;

per cases by A2;

suppose P . n in B ; :: thesis:

hence P ^ P2,n is_a_correct_step_wrt B,R by A1, FINSEQ_1:def 7; :: thesis:

end;

suppose ex Q being Formula-finset st
( [Q,(P . n)] in R & ( for t being object st t in Q holds
ex m being Nat st
( m in dom (P ^ P1) & m < n & (P ^ P1) . m = t ) ) ) ; :: thesis:

then consider Q being Formula-finset such that
A10: [Q,(P . n)] in R and
A11: for t being object st t in Q holds
ex m being Nat st
( m in dom (P ^ P1) & m < n & (P ^ P1) . m = t ) ;
A13: for t being object st t in Q holds
ex m being Nat st
( m in dom (P ^ P2) & m < n & (P ^ P2) . m = t )

proof

let t be object ; :: thesis:
assume t in Q ; :: thesis:
then consider m being Nat such that
A14: m in dom (P ^ P1) and
A15: m < n and
A16: (P ^ P1) . m = t by A11;
take m ; :: thesis:
A20: m in dom P by A1, A14, A15, Lm40;
dom P c= dom (P ^ P2) by FINSEQ_1:26;
hence m in dom (P ^ P2) by A1, A14, A15, Lm40; :: thesis:
thus m < n by A15; :: thesis:
thus (P ^ P2) . m = P . m by A20, FINSEQ_1:def 7
.= t by A16, A20, FINSEQ_1:def 7 ; :: thesis:

end;

thus P ^ P2,n is_a_correct_step_wrt B,R by A3, A10, A13; :: thesis:

end;

end;