let B be set ; :: thesis: for R being Rule
for t being object
for S being Formula-finset st ( for a being object st a in S holds
B,R |- a ) & [S,t] in R holds
B,R |- t
let R be Rule; :: thesis: for t being object
for S being Formula-finset st ( for a being object st a in S holds
B,R |- a ) & [S,t] in R holds
B,R |- t
let t be object ; :: thesis: for S being Formula-finset st ( for a being object st a in S holds
B,R |- a ) & [S,t] in R holds
B,R |- t
let S be Formula-finset; :: thesis: ( ( for a being object st a in S holds
B,R |- a ) & [S,t] in R implies B,R |- t )
assume that
A1: for a being object st a in S holds
B,R |- a and
A2: [S,t] in R ; :: thesis: B,R |- t
consider S1 being Formula-finset such that
A3: S c= S1 and
A4: S1 is B,R -derivable by A1, Th47;
consider P1 being Formula-sequence such that
A5: S1 = rng P1 and
A6: P1 is B,R -correct by A4;
set P2 = P1 ^ <*t*>;
take P1 ^ <*t*> ; :: according to PROOFS_1:def 10 :: thesis: ( t in rng (P1 ^ <*t*>) & P1 ^ <*t*> is B,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 (P1 ^ <*t*>) by FINSEQ_1:31; :: thesis: P1 ^ <*t*> is B,R -correct
let k be Nat; :: according to PROOFS_1:def 7 :: thesis: ( k in dom (P1 ^ <*t*>) implies P1 ^ <*t*>,k is_a_correct_step_wrt B,R )
assume k in dom (P1 ^ <*t*>) ; :: thesis: P1 ^ <*t*>,k is_a_correct_step_wrt B,R

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

suppose A11: k in dom P1 ; :: thesis: P1 ^ <*t*>,k is_a_correct_step_wrt B,R

then P1,k is_a_correct_step_wrt B,R by A6;
then P1 ^ (<*> {}),k is_a_correct_step_wrt B,R by FINSEQ_1:34;
hence P1 ^ <*t*>,k is_a_correct_step_wrt B,R by A11, Lm41; :: thesis: verum

end;

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

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

proof

let t be object ; :: thesis: ( t in S implies ex m being Nat st
( m in dom (P1 ^ <*t*>) & m < k & (P1 ^ <*t*>) . m = t ) )
assume t in S ; :: thesis: ex m being Nat st
( m in dom (P1 ^ <*t*>) & m < k & (P1 ^ <*t*>) . m = t )
then consider a being object such that
A25: a in dom P1 and
A26: P1 . a = t by A3, A5, FUNCT_1:def 3;
a in Seg (len P1) by A25, FINSEQ_1:def 3;
then reconsider m = a as Nat ;
take m ; :: thesis: ( m in dom (P1 ^ <*t*>) & m < k & (P1 ^ <*t*>) . m = t )
dom P1 c= dom (P1 ^ <*t*>) by FINSEQ_1:26;
hence m in dom (P1 ^ <*t*>) by A25; :: thesis: ( m < k & (P1 ^ <*t*>) . m = t )
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: (P1 ^ <*t*>) . m = t
thus (P1 ^ <*t*>) . m = t by A25, A26, FINSEQ_1:def 7; :: thesis: verum

end;

hence P1 ^ <*t*>,k is_a_correct_step_wrt B,R by A2, A22; :: thesis: verum

end;

end;