let X be set ; :: thesis: for S being Language
for D being RuleSet of S holds union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }
let S be Language; :: thesis: for D being RuleSet of S holds union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }
let D be RuleSet of S; :: thesis: union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }
set F = { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ;
set LH = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ;
set Q = S -sequents ;
set O = OneStep D;
set RH = union (((OneStep D) [*]) .: {X});

per cases ( not X in bool (S -sequents) or X in bool (S -sequents) ) ;

suppose C0: not X in bool (S -sequents) ; :: thesis: union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }

then {X} misses bool (S -sequents) by ZFMISC_1:50;
then {X} misses dom ((OneStep D) [*]) by XBOOLE_1:63;
then {X} /\ (dom ((OneStep D) [*])) = {} by XBOOLE_0:def 7;
then ((OneStep D) [*]) .: {X} = ((OneStep D) [*]) .: {} by RELAT_1:112
.= {} by RELAT_1:116 ;
then reconsider E = ((OneStep D) [*]) .: {X} as empty set ;

now

let x be set ; :: thesis: ( x in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } implies x in {{}} )
assume x in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ; :: thesis: x in {{}}
then consider mm being Element of NAT such that
E0: x = ((mm,D) -derivables) . X ;
not X in dom ((mm,D) -derivables) by C0;
then x = {} by E0, FUNCT_1:def 2;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

then { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } c= {{}} by TARSKI:def 3;
then union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } c= union {{}} by ZFMISC_1:77;
then union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } c= {} by ZFMISC_1:25;
then ( union E = {} & union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } = {} ) ;
hence union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ; :: thesis: verum

end;

suppose C0: X in bool (S -sequents) ; :: thesis: union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }

then reconsider Seqts = X as Element of bool (S -sequents) ;
for Y being set st Y in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } holds
Y c= union (((OneStep D) [*]) .: {X})

proof

let Y be set ; :: thesis: ( Y in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } implies Y c= union (((OneStep D) [*]) .: {X}) )
assume Y in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ; :: thesis: Y c= union (((OneStep D) [*]) .: {X})
then consider mm being Element of NAT such that
E0: Y = ((mm,D) -derivables) . X ;
thus Y c= union (((OneStep D) [*]) .: {X}) by E0, C0, Lm5; :: thesis: verum

end;

then C2: union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } c= union (((OneStep D) [*]) .: {X}) by ZFMISC_1:76;

now

let y be set ; :: thesis: ( y in union (((OneStep D) [*]) .: {X}) implies y in union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } )
assume y in union (((OneStep D) [*]) .: {X}) ; :: thesis: y in union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }
then {y} c= union (((OneStep D) [*]) .: {X}) by ZFMISC_1:31;
then {y} is Seqts,D -derivable by DefDerivable;
then consider mm being Element of NAT such that
E1: y is mm,Seqts,D -derivable by Lm3;
set Y = ((mm,D) -derivables) . Seqts;
( y in ((mm,D) -derivables) . Seqts & ((mm,D) -derivables) . Seqts in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ) by DefDerivable3, E1;
hence y in union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } by TARSKI:def 4; :: thesis: verum

end;

then union (((OneStep D) [*]) .: {X}) c= union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } by TARSKI:def 3;
hence union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } by C2, XBOOLE_0:def 10; :: thesis: verum

end;

end;