let m, n be Nat; :: thesis: for Z being set
for S being Language
for D1, D2 being RuleSet of S
for SQ1, SQ2 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 SQ1, SQ2 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 SQ1, SQ2 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 SQ1, SQ2 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 SQ1, SQ2 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 A1: ( 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 A2: ( SQ2 c= (iter ((OneStep D1),m)) . SQ1 & Z c= (iter ((OneStep D2),n)) . SQ2 ) ; :: thesis: Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1
A3: ( 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 Lm16, A1;
then A4: SQ2 c= ((m,(D1 \/ D2)) -derivables) . SQ1 by A2, XBOOLE_1:1;
A5: SQ1 in dom (iter ((OneStep (D1 \/ D2)),m)) by Lm1;
((n,D2) -derivables) . SQ2 c= ((n,(D1 \/ D2)) -derivables) . SQ2 by A3, A1, Lm16;
then A6: Z c= ((n,(D1 \/ D2)) -derivables) . SQ2 by A2, 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 FUNCT_1:13, A5 ;
then ((n,(D1 \/ D2)) -derivables) . SQ2 c= (((m + n),(D1 \/ D2)) -derivables) . SQ1 by A4, A1, Lm15;
hence Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1 by A6, XBOOLE_1:1; :: thesis: verum