let A be non empty Subset of GRZ-formula-set; :: thesis: for R being GRZ-rule
for P, P1, P2 being GRZ-formula-sequence
for n being Element of NAT st n in dom P & P ^ P1,n is_a_correct_step_wrt A,R holds
P ^ P2,n is_a_correct_step_wrt A,R
let R be GRZ-rule; :: thesis: for P, P1, P2 being GRZ-formula-sequence
for n being Element of NAT st n in dom P & P ^ P1,n is_a_correct_step_wrt A,R holds
P ^ P2,n is_a_correct_step_wrt A,R
let P, P1, P2 be GRZ-formula-sequence; :: thesis: for n being Element of NAT st n in dom P & P ^ P1,n is_a_correct_step_wrt A,R holds
P ^ P2,n is_a_correct_step_wrt A,R
let n be Element of NAT ; :: thesis: ( n in dom P & P ^ P1,n is_a_correct_step_wrt A,R implies P ^ P2,n is_a_correct_step_wrt A,R )
assume that
A1: n in dom P and
A2: P ^ P1,n is_a_correct_step_wrt A,R ; :: thesis: P ^ P2,n is_a_correct_step_wrt A,R
A3: P . n = (P ^ P1) . n by A1, FINSEQ_1:def 7;
A4: P . n = (P ^ P2) . n by A1, FINSEQ_1:def 7;

per cases ( P . n in A or ex Q being GRZ-formula-finset st
( [Q,(P . n)] in R & ( for q being FinSequence st q in Q holds
ex m being Element of NAT st
( m in dom (P ^ P1) & m < n & (P ^ P1) . m = q ) ) ) ) by A2, A3;

suppose P . n in A ; :: thesis: P ^ P2,n is_a_correct_step_wrt A,R

hence P ^ P2,n is_a_correct_step_wrt A,R by A4; :: thesis: verum

end;

suppose ex Q being GRZ-formula-finset st
( [Q,(P . n)] in R & ( for q being FinSequence st q in Q holds
ex m being Element of NAT st
( m in dom (P ^ P1) & m < n & (P ^ P1) . m = q ) ) ) ; :: thesis: P ^ P2,n is_a_correct_step_wrt A,R

then consider Q being GRZ-formula-finset such that
A10: [Q,(P . n)] in R and
A11: for q being FinSequence st q in Q holds
ex m being Element of NAT st
( m in dom (P ^ P1) & m < n & (P ^ P1) . m = q ) ;
A13: for q being FinSequence st q in Q holds
ex m being Element of NAT st
( m in dom (P ^ P2) & m < n & (P ^ P2) . m = q )

proof

let q be FinSequence; :: thesis: ( q in Q implies ex m being Element of NAT st
( m in dom (P ^ P2) & m < n & (P ^ P2) . m = q ) )
assume q in Q ; :: thesis: ex m being Element of NAT st
( m in dom (P ^ P2) & m < n & (P ^ P2) . m = q )
then consider m being Element of NAT such that
A14: m in dom (P ^ P1) and
A15: m < n and
A16: (P ^ P1) . m = q by A11;
take m ; :: thesis: ( m in dom (P ^ P2) & m < n & (P ^ P2) . m = q )
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 A20; :: thesis: ( m < n & (P ^ P2) . m = q )
thus m < n by A15; :: thesis: (P ^ P2) . m = q
thus (P ^ P2) . m = P . m by A20, FINSEQ_1:def 7
.= q by A16, A20, FINSEQ_1:def 7 ; :: thesis: verum

end;

thus P ^ P2,n is_a_correct_step_wrt A,R by A4, A10, A13; :: thesis: verum

end;

end;