let V, A be set ; :: thesis: for S1, S2 being FinSequence
for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S2 IsNDRankSeq V,A & S1 c= S2 & D1 in Union S1 & D2 in Union S2 holds
D1 \/ D2 in Union S2
let S1, S2 be FinSequence; :: thesis: for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S2 IsNDRankSeq V,A & S1 c= S2 & D1 in Union S1 & D2 in Union S2 holds
D1 \/ D2 in Union S2
let D1, D2 be NonatomicND of V,A; :: thesis: ( D1 tolerates D2 & S2 IsNDRankSeq V,A & S1 c= S2 & D1 in Union S1 & D2 in Union S2 implies D1 \/ D2 in Union S2 )
set D = D1 \/ D2;
set S = S1 +* S2;
A1: dom (S1 +* S2) = (dom S1) \/ (dom S2) by FUNCT_4:def 1;
assume that
A2: D1 tolerates D2 and
A3: S2 IsNDRankSeq V,A and
A4: S1 c= S2 and
A5: D1 in Union S1 and
A6: D2 in Union S2 ; :: thesis: D1 \/ D2 in Union S2
Union S1 c= Union S2 by A4, CARD_3:24;
then consider i being object such that
A7: i in dom S2 and
A8: D1 in S2 . i by A5, CARD_5:2;
consider j being object such that
A9: j in dom S2 and
A10: D2 in S2 . j by A6, CARD_5:2;
reconsider i = i as Element of NAT by A7;
reconsider j = j as Element of NAT by A9;
set k = max (i,j);
dom S1 c= dom S2 by A4, XTUPLE_0:8;
then A11: S1 +* S2 = S2 by FUNCT_4:19;
( max (i,j) in dom S1 or max (i,j) in dom S2 ) by A7, A9, XXREAL_0:16;
then A12: max (i,j) in dom (S1 +* S2) by A1, XBOOLE_0:def 3;
then A13: S2 . i c= S2 . (max (i,j)) by A3, A11, Th25, XXREAL_0:25;
S2 . j c= S2 . (max (i,j)) by A3, A11, A12, Th25, XXREAL_0:25;
hence D1 \/ D2 in Union S2 by A11, A12, A2, A3, A10, A8, A13, Th34, CARD_5:2; :: thesis: verum