let m be Nat; :: thesis: for X being set
for S being Language
for D being RuleSet of S st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let X be set ; :: thesis: for S being Language
for D being RuleSet of S st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let S be Language; :: thesis: for D being RuleSet of S st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let D be RuleSet of S; :: thesis: ( X c= S -sequents implies ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X}) )
set O = OneStep D;
set RH = union (((OneStep D) [*]) .: {X});
set Q = S -sequents ;
assume X c= S -sequents ; :: thesis: ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
then A1: X in dom (iter ((OneStep D),m)) by Lm1;
reconsider f = union {(iter ((OneStep D),m))} as Function ;
A2: (iter ((OneStep D),m)) . X = union {((iter ((OneStep D),m)) . X)}
.= union (Im ((iter ((OneStep D),m)),X)) by FUNCT_1:59, A1
.= union (f .: {X}) ;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
iter ((OneStep D),mm) = iter ((OneStep D),m) ;
then iter ((OneStep D),m) in D -iterators ;
then union {(iter ((OneStep D),m))} c= union (D -iterators) by ZFMISC_1:31, ZFMISC_1:77;
then f .: {X} c= (union (D -iterators)) .: {X} by RELAT_1:124;
then A3: ((m,D) -derivables) . X c= union ((union (D -iterators)) .: {X}) by A2, ZFMISC_1:77;
rng (OneStep D) c= dom (OneStep D) by Lm1;
hence ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X}) by A3, FOMODEL0:17; :: thesis: verum