let m, n be Nat; :: thesis: for Z being set
for S being Language
for D1, D2 being RuleSet of S
for SQ2, SQ1 being b₂ -sequents-like set st D1 is isotone & D1 \/ D2 is isotone & SQ2 c= (iter ((OneStep D1),m)) . SQ1 & Z c= (iter ((OneStep D2),n)) . SQ2 holds
Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1
let Z be set ; :: thesis: for S being Language
for D1, D2 being RuleSet of S
for SQ2, SQ1 being b₁ -sequents-like set st D1 is isotone & D1 \/ D2 is isotone & SQ2 c= (iter ((OneStep D1),m)) . SQ1 & Z c= (iter ((OneStep D2),n)) . SQ2 holds
Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1
let S be Language; :: thesis: for D1, D2 being RuleSet of S
for SQ2, SQ1 being S -sequents-like set st D1 is isotone & D1 \/ D2 is isotone & SQ2 c= (iter ((OneStep D1),m)) . SQ1 & Z c= (iter ((OneStep D2),n)) . SQ2 holds
Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1
let D1, D2 be RuleSet of S; :: thesis: for SQ2, SQ1 being S -sequents-like set st D1 is isotone & D1 \/ D2 is isotone & SQ2 c= (iter ((OneStep D1),m)) . SQ1 & Z c= (iter ((OneStep D2),n)) . SQ2 holds
Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1
let SQ2, SQ1 be S -sequents-like set ; :: thesis: ( D1 is isotone & D1 \/ D2 is isotone & SQ2 c= (iter ((OneStep D1),m)) . SQ1 & Z c= (iter ((OneStep D2),n)) . SQ2 implies Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1 )
reconsider mm = m, nn = n as Element of NAT by ORDINAL1:def 12;
set D3 = D1 \/ D2;
set O1 = OneStep D1;
set O2 = OneStep D2;
set O3 = OneStep (D1 \/ D2);
set X = SQ1;
set Y = SQ2;
assume B11: ( D1 is isotone & D1 \/ D2 is isotone ) ; :: thesis: ( not SQ2 c= (iter ((OneStep D1),m)) . SQ1 or not Z c= (iter ((OneStep D2),n)) . SQ2 or Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1 )
assume B0: ( SQ2 c= (iter ((OneStep D1),m)) . SQ1 & Z c= (iter ((OneStep D2),n)) . SQ2 ) ; :: thesis: Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1
B2: ( D1 \/ D2 c= D1 \/ D2 & D1 c= D1 \/ D2 & D2 c= D1 \/ D2 ) by XBOOLE_1:7;
then ((m,D1) -derivables) . SQ1 c= ((m,(D1 \/ D2)) -derivables) . SQ1 by Lm17, B11;
then BB3: SQ2 c= ((m,(D1 \/ D2)) -derivables) . SQ1 by B0, XBOOLE_1:1;
B6: SQ1 in dom (iter ((OneStep (D1 \/ D2)),m)) by Lm4;
((n,D2) -derivables) . SQ2 c= ((n,(D1 \/ D2)) -derivables) . SQ2 by B2, B11, Lm17;
then B5: Z c= ((n,(D1 \/ D2)) -derivables) . SQ2 by B0, XBOOLE_1:1;
(((m + n),(D1 \/ D2)) -derivables) . SQ1 = ((iter ((OneStep (D1 \/ D2)),nn)) * (iter ((OneStep (D1 \/ D2)),mm))) . SQ1 by FUNCT_7:77
.= ((n,(D1 \/ D2)) -derivables) . ((iter ((OneStep (D1 \/ D2)),m)) . SQ1) by B6, FUNCT_1:13 ;
then ((n,(D1 \/ D2)) -derivables) . SQ2 c= (((m + n),(D1 \/ D2)) -derivables) . SQ1 by BB3, B11, Lm15b;
hence Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1 by B5, XBOOLE_1:1; :: thesis: verum