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

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