let A be non empty set ; :: thesis: for R being Rule
for a being Element of A holds <*a*> is A,R -correct
let R be Rule; :: thesis: for a being Element of A holds <*a*> is A,R -correct
let a be Element of A; :: thesis: <*a*> is A,R -correct
set P = <*a*>;
let k be Nat; :: according to PROOFS_1:def 7 :: thesis: ( k in dom <*a*> implies <*a*>,k is_a_correct_step_wrt A,R )
assume k in dom <*a*> ; :: thesis: <*a*>,k is_a_correct_step_wrt A,R
then <*a*> . k in rng <*a*> by FUNCT_1:3;
then <*a*> . k in {a} by FINSEQ_1:38;
then <*a*> . k = a by TARSKI:def 1;
hence <*a*>,k is_a_correct_step_wrt A,R ; :: thesis: verum