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;

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;

end;

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;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