let m be Nat; :: thesis: for S being Language
for D being RuleSet of S
for R being Rule of S
for Seqts being Subset of (S -sequents)
for SQ being b₁ -sequents-like set holds
( dom (OneStep D) = bool (S -sequents) & rng (OneStep D) c= dom (OneStep D) & iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) & dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
let S be Language; :: thesis: for D being RuleSet of S
for R being Rule of S
for Seqts being Subset of (S -sequents)
for SQ being S -sequents-like set holds
( dom (OneStep D) = bool (S -sequents) & rng (OneStep D) c= dom (OneStep D) & iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) & dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
let D be RuleSet of S; :: thesis: for R being Rule of S
for Seqts being Subset of (S -sequents)
for SQ being S -sequents-like set holds
( dom (OneStep D) = bool (S -sequents) & rng (OneStep D) c= dom (OneStep D) & iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) & dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
let R be Rule of S; :: thesis: for Seqts being Subset of (S -sequents)
for SQ being S -sequents-like set holds
( dom (OneStep D) = bool (S -sequents) & rng (OneStep D) c= dom (OneStep D) & iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) & dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
let Seqts be Subset of (S -sequents); :: thesis: for SQ being S -sequents-like set holds
( dom (OneStep D) = bool (S -sequents) & rng (OneStep D) c= dom (OneStep D) & iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) & dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
let SQ be S -sequents-like set ; :: thesis: ( dom (OneStep D) = bool (S -sequents) & rng (OneStep D) c= dom (OneStep D) & iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) & dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
set O = OneStep D;
set Q = S -sequents ;
thus A1: dom (OneStep D) = bool (S -sequents) by FUNCT_2:def 1; :: thesis: ( rng (OneStep D) c= dom (OneStep D) & iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) & dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
hence rng (OneStep D) c= dom (OneStep D) by RELAT_1:def 19; :: thesis: ( iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) & dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
thus iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) by FUNCT_7:83; :: thesis: ( dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
hence dom (iter ((OneStep D),m)) = bool (S -sequents) by FUNCT_2:def 1; :: thesis: ( (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )
thus (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) by A1, XBOOLE_1:12, RELAT_1:def 19; :: thesis: ( Seqts in dom R & SQ in dom (iter (R,m)) )
dom R = bool (S -sequents) by FUNCT_2:def 1;
hence Seqts in dom R ; :: thesis: SQ in dom (iter (R,m))
iter (R,m) is Function of (bool (S -sequents)),(bool (S -sequents)) by FUNCT_7:83;
then ( dom (iter (R,m)) = bool (S -sequents) & SQ c= S -sequents ) by FUNCT_2:def 1, Def3;
hence SQ in dom (iter (R,m)) ; :: thesis: verum