let A be non empty Subset of GRZ-formula-set; :: thesis: for R being GRZ-rule
for t being GRZ-formula
for S being GRZ-formula-finset st A,R |- S & [S,t] in R holds
A,R |- t
let R be GRZ-rule; :: thesis: for t being GRZ-formula
for S being GRZ-formula-finset st A,R |- S & [S,t] in R holds
A,R |- t
let t be GRZ-formula; :: thesis: for S being GRZ-formula-finset st A,R |- S & [S,t] in R holds
A,R |- t
let S be GRZ-formula-finset; :: thesis: ( A,R |- S & [S,t] in R implies A,R |- t )
assume that
A1: A,R |- S and
A2: [S,t] in R ; :: thesis: A,R |- t
consider S1 being GRZ-formula-finset such that
A3: S c= S1 and
A4: S1 is A,R -correct by A1, Th47;
consider P1 being GRZ-formula-sequence such that
A5: S1 = rng P1 and
A6: P1 is A,R -correct by A4;
set P2 = P1 ^ <*t*>;
(rng P1) \/ (rng <*t*>) c= GRZ-formula-set by XBOOLE_1:8;
then rng (P1 ^ <*t*>) c= GRZ-formula-set by FINSEQ_1:31;
then reconsider P2 = P1 ^ <*t*> as GRZ-formula-sequence by FINSEQ_1:def 4;
take P2 ; :: according to GRZLOG_1:def 32 :: thesis: ( t in rng P2 & P2 is A,R -correct )
rng <*t*> = {t} by FINSEQ_1:38;
then t in rng <*t*> by TARSKI:def 1;
then t in (rng P1) \/ (rng <*t*>) by XBOOLE_0:def 3;
hence t in rng P2 by FINSEQ_1:31; :: thesis: P2 is A,R -correct
let k be Element of NAT ; :: according to GRZLOG_1:def 30 :: thesis: ( k in dom P2 implies P2,k is_a_correct_step_wrt A,R )
reconsider j = k as Nat ;
assume k in dom P2 ; :: thesis: P2,k is_a_correct_step_wrt A,R

per cases then ( j in dom P1 or ex i being Nat st
( i in dom <*t*> & j = (len P1) + i ) ) by FINSEQ_1:25;

suppose A11: j in dom P1 ; :: thesis: P2,k is_a_correct_step_wrt A,R

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

end;

suppose ex i being Nat st
( i in dom <*t*> & j = (len P1) + i ) ; :: thesis: P2,k is_a_correct_step_wrt A,R

then consider i being Nat such that
A20: i in dom <*t*> and
A21: j = (len P1) + i ;
P2 . j = <*t*> . i by A20, A21, FINSEQ_1:def 7;
then P2 . j in rng <*t*> by A20, FUNCT_1:3;
then P2 . j in {t} by FINSEQ_1:38;
then A22: P2 . j = t by TARSKI:def 1;
i in {1} by A20, FINSEQ_1:2, FINSEQ_1:def 8;
then A23: j = (len P1) + 1 by A21, TARSKI:def 1;
for q being FinSequence st q in S holds
ex m being Element of NAT st
( m in dom P2 & m < k & P2 . m = q )

proof

let q be FinSequence; :: thesis: ( q in S implies ex m being Element of NAT st
( m in dom P2 & m < k & P2 . m = q ) )
assume q in S ; :: thesis: ex m being Element of NAT st
( m in dom P2 & m < k & P2 . m = q )
then consider a being object such that
A25: a in dom P1 and
A26: P1 . a = q by A3, A5, FUNCT_1:def 3;
reconsider m = a as Element of NAT by A25;
take m ; :: thesis: ( m in dom P2 & m < k & P2 . m = q )
dom P1 c= dom P2 by FINSEQ_1:26;
hence m in dom P2 by A25; :: thesis: ( m < k & P2 . m = q )
m in Seg (len P1) by A25, FINSEQ_1:def 3;
then m <= len P1 by FINSEQ_1:1;
hence m < k by A23, NAT_1:13; :: thesis: P2 . m = q
thus P2 . m = q by A25, A26, FINSEQ_1:def 7; :: thesis: verum

end;

hence P2,k is_a_correct_step_wrt A,R by A2, A22; :: thesis: verum

end;

end;