let B be set ; :: thesis: for R being Rule
for S1, S2 being Formula-finset st S1 is B,R -derivable & S2 is S1,R -derivable holds
S1 \/ S2 is B,R -derivable
let R be Rule; :: thesis: for S1, S2 being Formula-finset st S1 is B,R -derivable & S2 is S1,R -derivable holds
S1 \/ S2 is B,R -derivable
let S1, S2 be Formula-finset; :: thesis: ( S1 is B,R -derivable & S2 is S1,R -derivable implies S1 \/ S2 is B,R -derivable )
assume ( S1 is B,R -derivable & S2 is S1,R -derivable ) ; :: thesis: S1 \/ S2 is B,R -derivable
then consider P1, P2 being Formula-sequence such that
A3: P1 is B,R -correct and
A4: S1 = rng P1 and
A5: P2 is S1,R -correct and
A6: S2 = rng P2 ;
set P = P1 ^ P2;
A8: for k being Nat st k in dom P1 holds
P1 ^ P2,k is_a_correct_step_wrt B,R

proof

let k be Nat; :: thesis: ( k in dom P1 implies P1 ^ P2,k is_a_correct_step_wrt B,R )
assume A9: k in dom P1 ; :: thesis: P1 ^ P2,k is_a_correct_step_wrt B,R
then P1,k is_a_correct_step_wrt B,R by A3;
then P1 ^ (<*> {}),k is_a_correct_step_wrt B,R by FINSEQ_1:34;
hence P1 ^ P2,k is_a_correct_step_wrt B,R by A9, Lm41; :: thesis: verum

end;

A10: P1 ^ P2 is B,R -correct

proof

let k be Nat; :: according to PROOFS_1:def 7 :: thesis: ( k in dom (P1 ^ P2) implies P1 ^ P2,k is_a_correct_step_wrt B,R )
assume k in dom (P1 ^ P2) ; :: thesis: P1 ^ P2,k is_a_correct_step_wrt B,R

per cases then ( k in dom P1 or ex i being Nat st
( i in dom P2 & k = (len P1) + i ) ) by FINSEQ_1:25;

suppose k in dom P1 ; :: thesis: P1 ^ P2,k is_a_correct_step_wrt B,R

hence P1 ^ P2,k is_a_correct_step_wrt B,R by A8; :: thesis: verum

end;

suppose ex i being Nat st
( i in dom P2 & k = (len P1) + i ) ; :: thesis: P1 ^ P2,k is_a_correct_step_wrt B,R

then consider i being Nat such that
A20: i in dom P2 and
A21: k = (len P1) + i ;
P2,i is_a_correct_step_wrt S1,R by A5, A20;

per cases then ( P2 . i in S1 or ex Q being Formula-finset st
( [Q,(P2 . i)] in R & ( for t being object st t in Q holds
ex l being Nat st
( l in dom P2 & l < i & P2 . l = t ) ) ) ) ;

suppose P2 . i in S1 ; :: thesis: P1 ^ P2,k is_a_correct_step_wrt B,R

then consider b being object such that
A25: b in dom P1 and
A26: P1 . b = P2 . i by A4, FUNCT_1:def 3;
A27: b in Seg (len P1) by A25, FINSEQ_1:def 3;
then reconsider n = b as Nat ;
A28: n <= len P1 by A27, FINSEQ_1:1;
k >= len P1 by A21, NAT_1:11;
then A29: n <= k by A28, XXREAL_0:2;
(P1 ^ P2) . n = P2 . i by A25, A26, FINSEQ_1:def 7
.= (P1 ^ P2) . k by A20, A21, FINSEQ_1:def 7 ;
hence P1 ^ P2,k is_a_correct_step_wrt B,R by A8, A25, A29, Lm52; :: thesis: verum

end;

suppose ex Q being Formula-finset st
( [Q,(P2 . i)] in R & ( for t being object st t in Q holds
ex l being Nat st
( l in dom P2 & l < i & P2 . l = t ) ) ) ; :: thesis: P1 ^ P2,k is_a_correct_step_wrt B,R

then consider Q being Formula-finset such that
A40: [Q,(P2 . i)] in R and
A41: for t being object st t in Q holds
ex l being Nat st
( l in dom P2 & l < i & P2 . l = t ) ;
A42: [Q,((P1 ^ P2) . k)] in R by A20, A21, A40, FINSEQ_1:def 7;
for t being object st t in Q holds
ex n being Nat st
( n in dom (P1 ^ P2) & n < k & (P1 ^ P2) . n = t )

proof

let t be object ; :: thesis: ( t in Q implies ex n being Nat st
( n in dom (P1 ^ P2) & n < k & (P1 ^ P2) . n = t ) )
assume t in Q ; :: thesis: ex n being Nat st
( n in dom (P1 ^ P2) & n < k & (P1 ^ P2) . n = t )
then consider l being Nat such that
A44: l in dom P2 and
A45: l < i and
A46: P2 . l = t by A41;
take n = l + (len P1); :: thesis: ( n in dom (P1 ^ P2) & n < k & (P1 ^ P2) . n = t )
thus n in dom (P1 ^ P2) by A44, FINSEQ_1:28; :: thesis: ( n < k & (P1 ^ P2) . n = t )
thus n < k by A21, A45, XREAL_1:6; :: thesis: (P1 ^ P2) . n = t
thus (P1 ^ P2) . n = t by A44, A46, FINSEQ_1:def 7; :: thesis: verum

end;

hence P1 ^ P2,k is_a_correct_step_wrt B,R by A42; :: thesis: verum

end;

end;

end;

end;

end;

reconsider S = rng (P1 ^ P2) as Formula-finset ;
S = S1 \/ S2 by A4, A6, FINSEQ_1:31;
hence S1 \/ S2 is B,R -derivable by A10; :: thesis: verum