let V be RealLinearSpace; :: thesis: for L1, L2 being circled_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
let L1, L2 be circled_Combination of V; :: thesis: for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
let a, b be Real; :: thesis: ( a * b > 0 implies Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) )
assume a * b > 0 ; :: thesis: Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
then A1: ( not ( a >= 0 & b <= 0 ) & not ( a <= 0 & b >= 0 ) ) ;
then A2: ( Carrier L1 = Carrier (a * L1) & Carrier L2 = Carrier (b * L2) ) by RLVECT_2:65;
for x being set st x in (Carrier (a * L1)) \/ (Carrier (b * L2)) holds
x in Carrier ((a * L1) + (b * L2))

proof

let x be set ; :: thesis: ( x in (Carrier (a * L1)) \/ (Carrier (b * L2)) implies x in Carrier ((a * L1) + (b * L2)) )
assume A3: x in (Carrier (a * L1)) \/ (Carrier (b * L2)) ; :: thesis: x in Carrier ((a * L1) + (b * L2))

per cases ( x in Carrier (a * L1) or x in Carrier (b * L2) ) by A3, XBOOLE_0:def 3;

suppose A4: x in Carrier (a * L1) ; :: thesis: x in Carrier ((a * L1) + (b * L2))

then x in { v where v is Element of V : (a * L1) . v <> 0 } by RLVECT_2:def 6;
then consider v being Element of V such that
A5: ( v = x & (a * L1) . v <> 0 ) ;
A6: L1 . v > 0 by A2, A4, A5, Th17;
v in Carrier ((a * L1) + (b * L2))

proof

per cases ( v in Carrier L2 or not v in Carrier L2 ) ;

suppose A7: v in Carrier L2 ; :: thesis: v in Carrier ((a * L1) + (b * L2))

then A8: L2 . v > 0 by Th17;

per cases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1;

suppose ( a > 0 & b > 0 ) ; :: thesis: v in Carrier ((a * L1) + (b * L2))

then ( a * (L1 . v) > 0 & b * (L2 . v) > 0 ) by A6, A8, XREAL_1:131;
then A9: ( (a * L1) . v > 0 & (b * L2) . v > 0 ) by RLVECT_2:def 13;
then ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:31;
then ((a * L1) + (b * L2)) . v > 0 by A9, RLVECT_2:def 12;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:28; :: thesis: verum

end;

suppose ( a < 0 & b < 0 ) ; :: thesis: v in Carrier ((a * L1) + (b * L2))

then ( a * (L1 . v) < 0 & b * (L2 . v) < 0 ) by A2, A4, A5, A7, Th17, XREAL_1:134;
then A10: ( (a * L1) . v < 0 & (b * L2) . v < 0 ) by RLVECT_2:def 13;
then ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:32;
then ((a * L1) + (b * L2)) . v < 0 by A10, RLVECT_2:def 12;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:28; :: thesis: verum

end;

end;

end;

suppose not v in Carrier L2 ; :: thesis: v in Carrier ((a * L1) + (b * L2))

then L2 . v = 0 by RLVECT_2:28;
then b * (L2 . v) = 0 ;
then (b * L2) . v = 0 by RLVECT_2:def 13;
then ((a * L1) . v) + ((b * L2) . v) = (a * L1) . v ;
then ((a * L1) + (b * L2)) . v <> 0 by A5, RLVECT_2:def 12;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:28; :: thesis: verum

end;

end;

end;

hence x in Carrier ((a * L1) + (b * L2)) by A5; :: thesis: verum

end;

suppose A11: x in Carrier (b * L2) ; :: thesis: x in Carrier ((a * L1) + (b * L2))

then x in { v where v is Element of V : (b * L2) . v <> 0 } by RLVECT_2:def 6;
then consider v being Element of V such that
A12: ( v = x & (b * L2) . v <> 0 ) ;
A13: L2 . v > 0 by A2, A11, A12, Th17;
v in Carrier ((a * L1) + (b * L2))

proof

per cases ( v in Carrier L1 or not v in Carrier L1 ) ;

suppose A14: v in Carrier L1 ; :: thesis: v in Carrier ((a * L1) + (b * L2))

then A15: L1 . v > 0 by Th17;

per cases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1;

suppose ( a > 0 & b > 0 ) ; :: thesis: v in Carrier ((a * L1) + (b * L2))

then ( a * (L1 . v) > 0 & b * (L2 . v) > 0 ) by A13, A15, XREAL_1:131;
then A16: ( (a * L1) . v > 0 & (b * L2) . v > 0 ) by RLVECT_2:def 13;
then ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:31;
then ((a * L1) + (b * L2)) . v > 0 by A16, RLVECT_2:def 12;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:28; :: thesis: verum

end;

suppose ( a < 0 & b < 0 ) ; :: thesis: v in Carrier ((a * L1) + (b * L2))

then ( a * (L1 . v) < 0 & b * (L2 . v) < 0 ) by A2, A11, A12, A14, Th17, XREAL_1:134;
then A17: ( (a * L1) . v < 0 & (b * L2) . v < 0 ) by RLVECT_2:def 13;
then ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:32;
then ((a * L1) + (b * L2)) . v < 0 by A17, RLVECT_2:def 12;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:28; :: thesis: verum

end;

end;

end;

suppose not v in Carrier L1 ; :: thesis: v in Carrier ((a * L1) + (b * L2))

then L1 . v = 0 by RLVECT_2:28;
then a * (L1 . v) = 0 ;
then (a * L1) . v = 0 by RLVECT_2:def 13;
then ((a * L1) . v) + ((b * L2) . v) = (b * L2) . v ;
then ((a * L1) + (b * L2)) . v <> 0 by A12, RLVECT_2:def 12;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:28; :: thesis: verum

end;

end;

end;

hence x in Carrier ((a * L1) + (b * L2)) by A12; :: thesis: verum

end;

end;

end;

then A18: (Carrier (a * L1)) \/ (Carrier (b * L2)) c= Carrier ((a * L1) + (b * L2)) by TARSKI:def 3;
Carrier ((a * L1) + (b * L2)) c= (Carrier (a * L1)) \/ (Carrier (b * L2)) by RLVECT_2:58;
hence Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by A18, XBOOLE_0:def 10; :: thesis: verum