let m, n be Nat; :: thesis: for y, X, z being set
for S being Language
for D1, D2 being RuleSet of S st D1 is isotone & D1 \/ D2 is isotone & y is m,X,D1 -derivable & z is n,{y},D2 -derivable holds
z is m + n,X,D1 \/ D2 -derivable
let y, X, z be set ; :: thesis: for S being Language
for D1, D2 being RuleSet of S st D1 is isotone & D1 \/ D2 is isotone & y is m,X,D1 -derivable & z is n,{y},D2 -derivable holds
z is m + n,X,D1 \/ D2 -derivable
let S be Language; :: thesis: for D1, D2 being RuleSet of S st D1 is isotone & D1 \/ D2 is isotone & y is m,X,D1 -derivable & z is n,{y},D2 -derivable holds
z is m + n,X,D1 \/ D2 -derivable
let D1, D2 be RuleSet of S; :: thesis: ( D1 is isotone & D1 \/ D2 is isotone & y is m,X,D1 -derivable & z is n,{y},D2 -derivable implies z is m + n,X,D1 \/ D2 -derivable )
set Q = S -sequents ;
set D3 = D1 \/ D2;
set O1 = OneStep D1;
set O2 = OneStep D2;
set O3 = OneStep (D1 \/ D2);
assume B2: ( D1 is isotone & D1 \/ D2 is isotone ) ; :: thesis: ( not y is m,X,D1 -derivable or not z is n,{y},D2 -derivable or z is m + n,X,D1 \/ D2 -derivable )
assume B0: ( y is m,X,D1 -derivable & z is n,{y},D2 -derivable ) ; :: thesis: z is m + n,X,D1 \/ D2 -derivable
then B1: ( y in ((m,D1) -derivables) . X & z in ((n,D2) -derivables) . {y} ) by DefDerivable3;
X in bool (S -sequents)

proof

assume not X in bool (S -sequents) ; :: thesis: contradiction
then not X in dom ((m,D1) -derivables) ;
then C1: ((m,D1) -derivables) . X = {} by FUNCT_1:def 2;
thus contradiction by C1, B0, DefDerivable3; :: thesis: verum

end;

then reconsider SQ = X as Subset of (S -sequents) ;
reconsider yy = y as Element of S -sequents by DefSeqtLike, B0;
( {yy} c= (iter ((OneStep D1),m)) . SQ & {z} c= (iter ((OneStep D2),n)) . {yy} ) by B1, ZFMISC_1:31;
then {z} c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ by Lm27, B2;
then z in (((m + n),(D1 \/ D2)) -derivables) . X by ZFMISC_1:31;
hence z is m + n,X,D1 \/ D2 -derivable by DefDerivable3; :: thesis: verum