let X be non empty addLoopStr ; :: thesis: for A, B being Subset of X

for l being Linear_Combination of A \/ B st A misses B holds

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

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

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A ) )

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

consider l1 being Linear_Combination of A such that

A3: ( Carrier l1 = (Carrier l) \ B & ( for x being Element of X st x in Carrier l1 holds

l1 . x = l . x ) ) by Th8;

consider l2 being Linear_Combination of B such that

A4: ( Carrier l2 = (Carrier l) \ A & ( for x being Element of X st x in Carrier l2 holds

l2 . x = l . x ) ) by Th8;

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

take l2 ; :: thesis: ( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

A5: (Carrier l1) \/ (Carrier l2) = (Carrier l) \ (A /\ B) by A3, A4, XBOOLE_1:54;

hence (Carrier l1) \/ (Carrier l2) = Carrier l by A2; :: thesis: ( l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

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

thus ( Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A ) by A3, A4; :: thesis: verum

for l being Linear_Combination of A \/ B st A misses B holds

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

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

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A ) )

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

consider l1 being Linear_Combination of A such that

A3: ( Carrier l1 = (Carrier l) \ B & ( for x being Element of X st x in Carrier l1 holds

l1 . x = l . x ) ) by Th8;

consider l2 being Linear_Combination of B such that

A4: ( Carrier l2 = (Carrier l) \ A & ( for x being Element of X st x in Carrier l2 holds

l2 . x = l . x ) ) by Th8;

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

( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

take l2 ; :: thesis: ( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

A5: (Carrier l1) \/ (Carrier l2) = (Carrier l) \ (A /\ B) by A3, A4, XBOOLE_1:54;

hence (Carrier l1) \/ (Carrier l2) = Carrier l by A2; :: thesis: ( l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

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

now :: thesis: for x being Element of X holds l . x = (l1 . x) + (l2 . x)

hence
l = l1 + l2
by RLVECT_2:def 10; :: thesis: ( Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )let x be Element of X; :: thesis: l . b_{1} = (l1 . b_{1}) + (l2 . b_{1})

end;per cases
( x in Carrier l1 or x in Carrier l2 or not x in Carrier l )
by A2, A5, XBOOLE_0:def 3;

end;

suppose A7:
x in Carrier l1
; :: thesis: l . b_{1} = (l1 . b_{1}) + (l2 . b_{1})

then
not x in Carrier l2
by A2, A6, XBOOLE_0:3;

then ( l1 . x = l . x & l2 . x = 0 ) by A3, A7;

hence l . x = (l1 . x) + (l2 . x) ; :: thesis: verum

end;then ( l1 . x = l . x & l2 . x = 0 ) by A3, A7;

hence l . x = (l1 . x) + (l2 . x) ; :: thesis: verum

thus ( Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A ) by A3, A4; :: thesis: verum