let V, A be set ; 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; 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; 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; ( 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 )
; 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;