let B be set ; :: thesis: for R being Rule
for P, P1, P2 being Formula-sequence st P is B,R -correct & P = P1 ^ P2 holds
P1 is B,R -correct
let R be Rule; :: thesis: for P, P1, P2 being Formula-sequence st P is B,R -correct & P = P1 ^ P2 holds
P1 is B,R -correct
let P, P1, P2 be Formula-sequence; :: thesis: ( P is B,R -correct & P = P1 ^ P2 implies P1 is B,R -correct )
assume that
A1: P is B,R -correct and
A2: P = P1 ^ P2 ; :: thesis: P1 is B,R -correct
let k be Nat; :: according to PROOFS_1:def 7 :: thesis: ( k in dom P1 implies P1,k is_a_correct_step_wrt B,R )
assume A3: k in dom P1 ; :: thesis: P1,k is_a_correct_step_wrt B,R
dom P1 c= dom P by A2, FINSEQ_1:26;
then P1 ^ (<*> {}),k is_a_correct_step_wrt B,R by A1, A2, A3, Lm41;
hence P1,k is_a_correct_step_wrt B,R by FINSEQ_1:34; :: thesis: verum