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

for l being Linear_Combination of A \/ B st rng l c= RAT & A misses B holds

ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) )

let A, B be Subset of X; :: thesis: for l being Linear_Combination of A \/ B st rng l c= RAT & A misses B holds

ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) )

let l be Linear_Combination of A \/ B; :: thesis: ( rng l c= RAT & A misses B implies ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) ) )

assume that

A1: rng l c= RAT and

A3: A misses B ; :: thesis: ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) )

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

A4: ( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A ) by A3, Th9;

take l1 ; :: thesis: ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) )

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

A5: ( Carrier l1 c= A & Carrier l2 c= B ) by RLVECT_2:def 6;

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

for l being Linear_Combination of A \/ B st rng l c= RAT & A misses B holds

ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) )

let A, B be Subset of X; :: thesis: for l being Linear_Combination of A \/ B st rng l c= RAT & A misses B holds

ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) )

let l be Linear_Combination of A \/ B; :: thesis: ( rng l c= RAT & A misses B implies ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) ) )

assume that

A1: rng l c= RAT and

A3: A misses B ; :: thesis: ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) )

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

A4: ( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A ) by A3, Th9;

take l1 ; :: thesis: ex l2 being Linear_Combination of B st

( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) )

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

A5: ( Carrier l1 c= A & Carrier l2 c= B ) by RLVECT_2:def 6;

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

y in RAT

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

let y be object ; :: thesis: ( y in rng l1 implies b_{1} in RAT )

assume y in rng l1 ; :: thesis: b_{1} in RAT

then consider x being object such that

A6: ( x in dom l1 & y = l1 . x ) by FUNCT_1:def 3;

x in the carrier of X by A6;

then ( x in dom l & x in dom l2 ) by FUNCT_2:def 1;

then A7: ( l . x in rng l & l2 . x in rng l2 & l . x = (l1 . x) + (l2 . x) ) by A4, FUNCT_1:3, RLVECT_2:def 10;

end;assume y in rng l1 ; :: thesis: b

then consider x being object such that

A6: ( x in dom l1 & y = l1 . x ) by FUNCT_1:def 3;

x in the carrier of X by A6;

then ( x in dom l & x in dom l2 ) by FUNCT_2:def 1;

then A7: ( l . x in rng l & l2 . x in rng l2 & l . x = (l1 . x) + (l2 . x) ) by A4, FUNCT_1:3, RLVECT_2:def 10;

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

y in RAT

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

let y be object ; :: thesis: ( y in rng l2 implies b_{1} in RAT )

assume y in rng l2 ; :: thesis: b_{1} in RAT

then consider x being object such that

A8: ( x in dom l2 & y = l2 . x ) by FUNCT_1:def 3;

x in the carrier of X by A8;

then ( x in dom l & x in dom l1 ) by FUNCT_2:def 1;

then A9: ( l . x in rng l & l1 . x in rng l1 & l . x = (l1 . x) + (l2 . x) ) by A4, FUNCT_1:3, RLVECT_2:def 10;

end;assume y in rng l2 ; :: thesis: b

then consider x being object such that

A8: ( x in dom l2 & y = l2 . x ) by FUNCT_1:def 3;

x in the carrier of X by A8;

then ( x in dom l & x in dom l1 ) by FUNCT_2:def 1;

then A9: ( l . x in rng l & l1 . x in rng l1 & l . x = (l1 . x) + (l2 . x) ) by A4, FUNCT_1:3, RLVECT_2:def 10;

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