let X be RealLinearSpace; :: thesis: for A, B being finite Subset of X st A misses B holds

(RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B)

let A, B be finite Subset of X; :: thesis: ( A misses B implies (RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B) )

assume A3: A misses B ; :: thesis: (RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B)

set D1 = RAT_Sums A;

set D2 = RAT_Sums B;

set S1 = (RAT_Sums A) + (RAT_Sums B);

set S2 = RAT_Sums (A \/ B);

A4: (RAT_Sums A) + (RAT_Sums B) = { (a + b) where a, b is Point of X : ( a in RAT_Sums A & b in RAT_Sums B ) } by IDEAL_1:def 19;

hence (RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B) by A8; :: thesis: verum

(RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B)

let A, B be finite Subset of X; :: thesis: ( A misses B implies (RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B) )

assume A3: A misses B ; :: thesis: (RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B)

set D1 = RAT_Sums A;

set D2 = RAT_Sums B;

set S1 = (RAT_Sums A) + (RAT_Sums B);

set S2 = RAT_Sums (A \/ B);

A4: (RAT_Sums A) + (RAT_Sums B) = { (a + b) where a, b is Point of X : ( a in RAT_Sums A & b in RAT_Sums B ) } by IDEAL_1:def 19;

now :: thesis: for p being object st p in (RAT_Sums A) + (RAT_Sums B) holds

p in RAT_Sums (A \/ B)

then A8:
(RAT_Sums A) + (RAT_Sums B) c= RAT_Sums (A \/ B)
;p in RAT_Sums (A \/ B)

let p be object ; :: thesis: ( p in (RAT_Sums A) + (RAT_Sums B) implies p in RAT_Sums (A \/ B) )

assume p in (RAT_Sums A) + (RAT_Sums B) ; :: thesis: p in RAT_Sums (A \/ B)

then consider a, b being Point of X such that

A5: ( p = a + b & a in RAT_Sums A & b in RAT_Sums B ) by A4;

consider l1 being Linear_Combination of A such that

A6: ( a = Sum l1 & rng l1 c= RAT ) by A5;

consider l2 being Linear_Combination of B such that

A7: ( b = Sum l2 & rng l2 c= RAT ) by A5;

ex l being Linear_Combination of A \/ B st

( Carrier l = (Carrier l1) \/ (Carrier l2) & rng l c= RAT & Sum l = (Sum l1) + (Sum l2) ) by A3, A6, A7, Th10;

hence p in RAT_Sums (A \/ B) by A5, A6, A7; :: thesis: verum

end;assume p in (RAT_Sums A) + (RAT_Sums B) ; :: thesis: p in RAT_Sums (A \/ B)

then consider a, b being Point of X such that

A5: ( p = a + b & a in RAT_Sums A & b in RAT_Sums B ) by A4;

consider l1 being Linear_Combination of A such that

A6: ( a = Sum l1 & rng l1 c= RAT ) by A5;

consider l2 being Linear_Combination of B such that

A7: ( b = Sum l2 & rng l2 c= RAT ) by A5;

ex l being Linear_Combination of A \/ B st

( Carrier l = (Carrier l1) \/ (Carrier l2) & rng l c= RAT & Sum l = (Sum l1) + (Sum l2) ) by A3, A6, A7, Th10;

hence p in RAT_Sums (A \/ B) by A5, A6, A7; :: thesis: verum

now :: thesis: for p being object st p in RAT_Sums (A \/ B) holds

p in (RAT_Sums A) + (RAT_Sums B)

then
RAT_Sums (A \/ B) c= (RAT_Sums A) + (RAT_Sums B)
;p in (RAT_Sums A) + (RAT_Sums B)

let p be object ; :: thesis: ( p in RAT_Sums (A \/ B) implies p in (RAT_Sums A) + (RAT_Sums B) )

assume p in RAT_Sums (A \/ B) ; :: thesis: p in (RAT_Sums A) + (RAT_Sums B)

then consider l being Linear_Combination of A \/ B such that

A9: ( p = Sum l & rng l c= RAT ) ;

consider l1 being Linear_Combination of A, l2 being Linear_Combination of B such that

A10: ( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) ) by A3, A9, Th11;

( Sum l1 in RAT_Sums A & Sum l2 in RAT_Sums B ) by A10;

hence p in (RAT_Sums A) + (RAT_Sums B) by A4, A9, A10; :: thesis: verum

end;assume p in RAT_Sums (A \/ B) ; :: thesis: p in (RAT_Sums A) + (RAT_Sums B)

then consider l being Linear_Combination of A \/ B such that

A9: ( p = Sum l & rng l c= RAT ) ;

consider l1 being Linear_Combination of A, l2 being Linear_Combination of B such that

A10: ( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) ) by A3, A9, Th11;

( Sum l1 in RAT_Sums A & Sum l2 in RAT_Sums B ) by A10;

hence p in (RAT_Sums A) + (RAT_Sums B) by A4, A9, A10; :: thesis: verum

hence (RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B) by A8; :: thesis: verum