let X be RealLinearSpace; :: thesis: for A, B being Subset of X

for l1 being Linear_Combination of A

for l2 being Linear_Combination of B st rng l1 c= RAT & rng l2 c= RAT & A misses B holds

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) )

let A, B be Subset of X; :: thesis: for l1 being Linear_Combination of A

for l2 being Linear_Combination of B st rng l1 c= RAT & rng l2 c= RAT & A misses B holds

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) )

let l1 be Linear_Combination of A; :: thesis: for l2 being Linear_Combination of B st rng l1 c= RAT & rng l2 c= RAT & A misses B holds

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) )

let l2 be Linear_Combination of B; :: thesis: ( rng l1 c= RAT & rng l2 c= RAT & A misses B implies 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) ) )

assume that

A1: ( rng l1 c= RAT & rng l2 c= RAT ) and

A2: A misses B ; :: thesis: 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) )

consider l being Linear_Combination of A \/ B such that

A3: ( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 ) by A2, Th7;

take l ; :: thesis: ( Carrier l = (Carrier l1) \/ (Carrier l2) & rng l c= RAT & Sum l = (Sum l1) + (Sum l2) )

thus Carrier l = (Carrier l1) \/ (Carrier l2) by A3; :: thesis: ( rng l c= RAT & Sum l = (Sum l1) + (Sum l2) )

thus Sum l = (Sum l1) + (Sum l2) by A3, RLVECT_3:1; :: thesis: verum

for l1 being Linear_Combination of A

for l2 being Linear_Combination of B st rng l1 c= RAT & rng l2 c= RAT & A misses B holds

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) )

let A, B be Subset of X; :: thesis: for l1 being Linear_Combination of A

for l2 being Linear_Combination of B st rng l1 c= RAT & rng l2 c= RAT & A misses B holds

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) )

let l1 be Linear_Combination of A; :: thesis: for l2 being Linear_Combination of B st rng l1 c= RAT & rng l2 c= RAT & A misses B holds

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) )

let l2 be Linear_Combination of B; :: thesis: ( rng l1 c= RAT & rng l2 c= RAT & A misses B implies 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) ) )

assume that

A1: ( rng l1 c= RAT & rng l2 c= RAT ) and

A2: A misses B ; :: thesis: 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) )

consider l being Linear_Combination of A \/ B such that

A3: ( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 ) by A2, Th7;

take l ; :: thesis: ( Carrier l = (Carrier l1) \/ (Carrier l2) & rng l c= RAT & Sum l = (Sum l1) + (Sum l2) )

thus Carrier l = (Carrier l1) \/ (Carrier l2) by A3; :: thesis: ( rng l c= RAT & Sum l = (Sum l1) + (Sum l2) )

now :: thesis: for y being object st y in rng l holds

y in RAT

hence
rng l c= RAT
; :: thesis: Sum l = (Sum l1) + (Sum l2)y in RAT

let y be object ; :: thesis: ( y in rng l implies y in RAT )

assume y in rng l ; :: thesis: y in RAT

then consider x being object such that

A4: ( x in dom l & y = l . x ) by FUNCT_1:def 3;

A5: x in the carrier of X by A4;

A6: l . x = (l1 . x) + (l2 . x) by A3, A4, RLVECT_2:def 10;

( x in dom l1 & x in dom l2 ) by A5, FUNCT_2:def 1;

then ( l1 . x in rng l1 & l2 . x in rng l2 ) by FUNCT_1:3;

hence y in RAT by A1, A4, A6, RAT_1:def 2; :: thesis: verum

end;assume y in rng l ; :: thesis: y in RAT

then consider x being object such that

A4: ( x in dom l & y = l . x ) by FUNCT_1:def 3;

A5: x in the carrier of X by A4;

A6: l . x = (l1 . x) + (l2 . x) by A3, A4, RLVECT_2:def 10;

( x in dom l1 & x in dom l2 ) by A5, FUNCT_2:def 1;

then ( l1 . x in rng l1 & l2 . x in rng l2 ) by FUNCT_1:3;

hence y in RAT by A1, A4, A6, RAT_1:def 2; :: thesis: verum

thus Sum l = (Sum l1) + (Sum l2) by A3, RLVECT_3:1; :: thesis: verum