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;
now :: thesis: for p being object st p in (RAT_Sums A) + (RAT_Sums B) holds
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;
then A8: (RAT_Sums A) + (RAT_Sums B) c= RAT_Sums (A \/ B) ;
now :: thesis: for p being object st p in RAT_Sums (A \/ B) holds
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;
then RAT_Sums (A \/ B) c= (RAT_Sums A) + (RAT_Sums B) ;
hence (RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B) by A8; :: thesis: verum