let V, A be set ; :: thesis: for m being Nat
for S being FinSequence
for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S IsNDRankSeq V,A & D1 in S . m & D2 in S . m holds
D1 \/ D2 in S . m
let m be Nat; :: thesis: for S being FinSequence
for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S IsNDRankSeq V,A & D1 in S . m & D2 in S . m holds
D1 \/ D2 in S . m
let S be FinSequence; :: thesis: for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S IsNDRankSeq V,A & D1 in S . m & D2 in S . m holds
D1 \/ D2 in S . m
let D1, D2 be NonatomicND of V,A; :: thesis: ( D1 tolerates D2 & S IsNDRankSeq V,A & D1 in S . m & D2 in S . m implies D1 \/ D2 in S . m )
set D = D1 \/ D2;
assume that
A1: D1 tolerates D2 and
A2: S IsNDRankSeq V,A and
A3: ( D1 in S . m & D2 in S . m ) ; :: thesis: D1 \/ D2 in S . m
A4: m in dom S by A3, FUNCT_1:def 2;
not 0 in dom S by FINSEQ_3:24;
then m <> 0 by A3, FUNCT_1:def 2;
then A5: 0 + 1 <= m by NAT_1:13;
then reconsider z = m - 1 as Element of NAT by INT_1:5;

per cases ( 1 < m or m = 1 ) by A5, XXREAL_0:1;

suppose 1 < m ; :: thesis: D1 \/ D2 in S . m

then A6: S . (z + 1) = NDSS (V,(A \/ (S . z))) by A2, A4, CGAMES_1:20;
then ( D1 is PartFunc of V,(A \/ (S . z)) & D2 is PartFunc of V,(A \/ (S . z)) ) by A3, Th4;
then ( D1 \/ D2 is V -defined & D1 \/ D2 is A \/ (S . z) -valued ) ;
then D1 \/ D2 is PartFunc of V,(A \/ (S . z)) by A1, RELSET_1:4, PARTFUN1:51;
hence D1 \/ D2 in S . m by A6; :: thesis: verum

end;

suppose m = 1 ; :: thesis: D1 \/ D2 in S . m

hence D1 \/ D2 in S . m by A1, A2, A3, Th8; :: thesis: verum

end;

end;