let m, n be Nat; :: thesis: for X being set
for S being Language
for D1, D2 being RuleSet of S
for y, z being object 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 X be set ; :: thesis: for S being Language
for D1, D2 being RuleSet of S
for y, z being object 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
for y, z being object 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: for y, z being object 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, z be object ; :: 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 A1: ( 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 A2: ( y is m,X,D1 -derivable & z is n,{y},D2 -derivable ) ; :: thesis: z is m + n,X,D1 \/ D2 -derivable
then A3: ( y in ((m,D1) -derivables) . X & z in ((n,D2) -derivables) . {y} ) ;
X in bool (S -sequents)

proof

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

end;

then reconsider SQ = X as Subset of (S -sequents) ;
y is S -sequent-like by A2;
then reconsider yy = y as Element of S -sequents ;
( {yy} c= (iter ((OneStep D1),m)) . SQ & {z} c= (iter ((OneStep D2),n)) . {yy} ) by ZFMISC_1:31, A3;
then z in (((m + n),(D1 \/ D2)) -derivables) . X by Lm21, A1, ZFMISC_1:31;
hence z is m + n,X,D1 \/ D2 -derivable ; :: thesis: verum