let m, n be Nat; :: thesis: for x, y, z being set
for S being Language
for D1, D2, D3 being RuleSet of S
for SQ1, SQ2 being b₄ -sequents-like set st D1 \/ D2 is isotone & (D1 \/ D2) \/ D3 is isotone & x is m,SQ1,D1 -derivable & y is m,SQ2,D2 -derivable & z is n,{x,y},D3 -derivable holds
z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable
let x, y, z be set ; :: thesis: for S being Language
for D1, D2, D3 being RuleSet of S
for SQ1, SQ2 being b₁ -sequents-like set st D1 \/ D2 is isotone & (D1 \/ D2) \/ D3 is isotone & x is m,SQ1,D1 -derivable & y is m,SQ2,D2 -derivable & z is n,{x,y},D3 -derivable holds
z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable
let S be Language; :: thesis: for D1, D2, D3 being RuleSet of S
for SQ1, SQ2 being S -sequents-like set st D1 \/ D2 is isotone & (D1 \/ D2) \/ D3 is isotone & x is m,SQ1,D1 -derivable & y is m,SQ2,D2 -derivable & z is n,{x,y},D3 -derivable holds
z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable
let D1, D2, D3 be RuleSet of S; :: thesis: for SQ1, SQ2 being S -sequents-like set st D1 \/ D2 is isotone & (D1 \/ D2) \/ D3 is isotone & x is m,SQ1,D1 -derivable & y is m,SQ2,D2 -derivable & z is n,{x,y},D3 -derivable holds
z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable
let SQ1, SQ2 be S -sequents-like set ; :: thesis: ( D1 \/ D2 is isotone & (D1 \/ D2) \/ D3 is isotone & x is m,SQ1,D1 -derivable & y is m,SQ2,D2 -derivable & z is n,{x,y},D3 -derivable implies z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable )
set Q = S -sequents ;
set D = D1 \/ D2;
set O1 = OneStep D1;
set O2 = OneStep D2;
set O3 = OneStep D3;
set O = OneStep (D1 \/ D2);
set OO = OneStep ((D1 \/ D2) \/ D3);
reconsider X = SQ1, Y = SQ2 as Subset of (S -sequents) by DefSeqtLike2;
set Z = X \/ Y;
assume B1: ( D1 \/ D2 is isotone & (D1 \/ D2) \/ D3 is isotone ) ; :: thesis: ( not x is m,SQ1,D1 -derivable or not y is m,SQ2,D2 -derivable or not z is n,{x,y},D3 -derivable or z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable )
assume B3: ( x is m,SQ1,D1 -derivable & y is m,SQ2,D2 -derivable ) ; :: thesis: ( not z is n,{x,y},D3 -derivable or z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable )
then BB2: ( x in ((m,D1) -derivables) . X & y in ((m,D2) -derivables) . Y ) by DefDerivable3;
reconsider sq1 = x, sq2 = y as S -sequent-like set by B3;
( X null Y c= X \/ Y & Y null X c= X \/ Y & D1 null D2 c= D1 \/ D2 & D2 null D1 c= D1 \/ D2 ) ;
then ( ((m,D1) -derivables) . X c= ((m,(D1 \/ D2)) -derivables) . (X \/ Y) & ((m,D2) -derivables) . Y c= ((m,(D1 \/ D2)) -derivables) . (X \/ Y) ) by Lm15, B1;
then B0: {sq1,sq2} c= (iter ((OneStep (D1 \/ D2)),m)) . (X \/ Y) by BB2, ZFMISC_1:32;
assume z is n,{x,y},D3 -derivable ; :: thesis: z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable
then z in ((n,D3) -derivables) . {x,y} by DefDerivable3;
then {z} c= (iter ((OneStep D3),n)) . {x,y} by ZFMISC_1:31;
then {z} c= (iter ((OneStep ((D1 \/ D2) \/ D3)),(m + n))) . (X \/ Y) by B0, B1, Lm27;
then z in (((m + n),((D1 \/ D2) \/ D3)) -derivables) . (X \/ Y) by ZFMISC_1:31;
hence z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable by DefDerivable3; :: thesis: verum