let K be Ring; :: thesis: for V being VectSp of K

for A1, A2 being Subset of V

for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds

ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

let V be VectSp of K; :: thesis: for A1, A2 being Subset of V

for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds

ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

let A1, A2 be Subset of V; :: thesis: for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds

ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

let l be Linear_Combination of A1 \/ A2; :: thesis: ( A1 /\ A2 = {} implies ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2 )

assume A1: A1 /\ A2 = {} ; :: thesis: ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

A2: A1 misses A2 by A1;

defpred S_{1}[ object , object ] means ( not $1 is Vector of V or ( $1 in A1 & $2 = l . $1 ) or ( not $1 in A1 & $2 = 0. K ) );

A3: for x being object st x in the carrier of V holds

ex y being object st

( y in the carrier of K & S_{1}[x,y] )

for x being object st x in the carrier of V holds

S_{1}[x,l1 . x]
from FUNCT_2:sch 1(A3);

then consider l1 being Function of the carrier of V, the carrier of K such that

A4: for x being object st x in the carrier of V holds

S_{1}[x,l1 . x]
;

reconsider l1 = l1 as Linear_Combination of V by A5, VECTSP_6:def 1;

for x being object st x in Carrier l1 holds

x in A1

defpred S_{2}[ object , object ] means ( not $1 is Vector of V or ( $1 in A2 & $2 = l . $1 ) or ( not $1 in A2 & $2 = 0. K ) );

A7: for x being object st x in the carrier of V holds

ex y being object st

( y in the carrier of K & S_{2}[x,y] )

for x being object st x in the carrier of V holds

S_{2}[x,l2 . x]
from FUNCT_2:sch 1(A7);

then consider l2 being Function of the carrier of V, the carrier of K such that

A8: for x being object st x in the carrier of V holds

S_{2}[x,l2 . x]
;

reconsider l2 = l2 as Linear_Combination of V by A9, VECTSP_6:def 1;

for x being object st x in Carrier l2 holds

x in A2

for v being Vector of V holds l . v = (l1 + l2) . v

for A1, A2 being Subset of V

for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds

ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

let V be VectSp of K; :: thesis: for A1, A2 being Subset of V

for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds

ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

let A1, A2 be Subset of V; :: thesis: for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds

ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

let l be Linear_Combination of A1 \/ A2; :: thesis: ( A1 /\ A2 = {} implies ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2 )

assume A1: A1 /\ A2 = {} ; :: thesis: ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

A2: A1 misses A2 by A1;

defpred S

A3: for x being object st x in the carrier of V holds

ex y being object st

( y in the carrier of K & S

proof

ex l1 being Function of the carrier of V, the carrier of K st
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st

( y in the carrier of K & S_{1}[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S_{1}[x,y] )

then reconsider x9 = x as Vector of V ;

end;( y in the carrier of K & S

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S

then reconsider x9 = x as Vector of V ;

per cases
( x in A1 or not x in A1 )
;

end;

suppose B1:
x in A1
; :: thesis: ex y being object st

( y in the carrier of K & S_{1}[x,y] )

( y in the carrier of K & S

l . x9 in the carrier of K
;

hence ex y being object st

( y in the carrier of K & S_{1}[x,y] )
by B1; :: thesis: verum

end;hence ex y being object st

( y in the carrier of K & S

for x being object st x in the carrier of V holds

S

then consider l1 being Function of the carrier of V, the carrier of K such that

A4: for x being object st x in the carrier of V holds

S

A5: now :: thesis: for v being Vector of V st not v in A1 /\ (Carrier l) holds

l1 . v = 0. K

reconsider l1 = l1 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;l1 . v = 0. K

let v be Vector of V; :: thesis: ( not v in A1 /\ (Carrier l) implies l1 . b_{1} = 0. K )

assume A6: not v in A1 /\ (Carrier l) ; :: thesis: l1 . b_{1} = 0. K

end;assume A6: not v in A1 /\ (Carrier l) ; :: thesis: l1 . b

reconsider l1 = l1 as Linear_Combination of V by A5, VECTSP_6:def 1;

for x being object st x in Carrier l1 holds

x in A1

proof

then AX1:
l1 is Linear_Combination of A1
by TARSKI:def 3, VECTSP_6:def 4;
let x be object ; :: thesis: ( x in Carrier l1 implies x in A1 )

assume B1: x in Carrier l1 ; :: thesis: x in A1

then reconsider x = x as Vector of V ;

l1 . x <> 0. K by B1, VECTSP_6:2;

hence x in A1 by A4; :: thesis: verum

end;assume B1: x in Carrier l1 ; :: thesis: x in A1

then reconsider x = x as Vector of V ;

l1 . x <> 0. K by B1, VECTSP_6:2;

hence x in A1 by A4; :: thesis: verum

defpred S

A7: for x being object st x in the carrier of V holds

ex y being object st

( y in the carrier of K & S

proof

ex l2 being Function of the carrier of V, the carrier of K st
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st

( y in the carrier of K & S_{2}[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S_{2}[x,y] )

then reconsider x9 = x as Vector of V ;

end;( y in the carrier of K & S

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S

then reconsider x9 = x as Vector of V ;

per cases
( x in A2 or not x in A2 )
;

end;

suppose B1:
x in A2
; :: thesis: ex y being object st

( y in the carrier of K & S_{2}[x,y] )

( y in the carrier of K & S

l . x9 in the carrier of K
;

hence ex y being object st

( y in the carrier of K & S_{2}[x,y] )
by B1; :: thesis: verum

end;hence ex y being object st

( y in the carrier of K & S

for x being object st x in the carrier of V holds

S

then consider l2 being Function of the carrier of V, the carrier of K such that

A8: for x being object st x in the carrier of V holds

S

A9: now :: thesis: for v being Vector of V st not v in A2 /\ (Carrier l) holds

l2 . v = 0. K

reconsider l2 = l2 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;l2 . v = 0. K

let v be Vector of V; :: thesis: ( not v in A2 /\ (Carrier l) implies l2 . b_{1} = 0. K )

assume A10: not v in A2 /\ (Carrier l) ; :: thesis: l2 . b_{1} = 0. K

end;assume A10: not v in A2 /\ (Carrier l) ; :: thesis: l2 . b

reconsider l2 = l2 as Linear_Combination of V by A9, VECTSP_6:def 1;

for x being object st x in Carrier l2 holds

x in A2

proof

then AX2:
l2 is Linear_Combination of A2
by TARSKI:def 3, VECTSP_6:def 4;
let x be object ; :: thesis: ( x in Carrier l2 implies x in A2 )

assume B1: x in Carrier l2 ; :: thesis: x in A2

then reconsider x = x as Vector of V ;

l2 . x <> 0. K by B1, VECTSP_6:2;

hence x in A2 by A8; :: thesis: verum

end;assume B1: x in Carrier l2 ; :: thesis: x in A2

then reconsider x = x as Vector of V ;

l2 . x <> 0. K by B1, VECTSP_6:2;

hence x in A2 by A8; :: thesis: verum

for v being Vector of V holds l . v = (l1 + l2) . v

proof

hence
ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2
by AX1, AX2, VECTSP_6:def 7; :: thesis: verum
let v be Vector of V; :: thesis: l . v = (l1 + l2) . v

end;per cases
( v in A1 or v in A2 or ( not v in A1 & not v in A2 ) )
;

end;

suppose B1:
v in A1
; :: thesis: l . v = (l1 + l2) . v

then
v in A1 \/ A2
by XBOOLE_0:def 3;

then B2: not v in A2 by A2, B1, XBOOLE_0:5;

thus l . v = (l1 . v) + (0. K) by A4, B1

.= (l1 . v) + (l2 . v) by A8, B2

.= (l1 + l2) . v by VECTSP_6:22 ; :: thesis: verum

end;then B2: not v in A2 by A2, B1, XBOOLE_0:5;

thus l . v = (l1 . v) + (0. K) by A4, B1

.= (l1 . v) + (l2 . v) by A8, B2

.= (l1 + l2) . v by VECTSP_6:22 ; :: thesis: verum

suppose B1:
v in A2
; :: thesis: l . v = (l1 + l2) . v

then
v in A1 \/ A2
by XBOOLE_0:def 3;

then B2: not v in A1 by A2, B1, XBOOLE_0:5;

thus l . v = (0. K) + (l2 . v) by A8, B1

.= (l1 . v) + (l2 . v) by A4, B2

.= (l1 + l2) . v by VECTSP_6:22 ; :: thesis: verum

end;then B2: not v in A1 by A2, B1, XBOOLE_0:5;

thus l . v = (0. K) + (l2 . v) by A8, B1

.= (l1 . v) + (l2 . v) by A4, B2

.= (l1 + l2) . v by VECTSP_6:22 ; :: thesis: verum

suppose B1:
( not v in A1 & not v in A2 )
; :: thesis: l . v = (l1 + l2) . v

then
not v in A1 \/ A2
by XBOOLE_0:def 3;

then not v in Carrier l by TARSKI:def 3, VECTSP_6:def 4;

hence l . v = 0. K

.= (l1 . v) + (0. K) by A4, B1

.= (l1 . v) + (l2 . v) by A8, B1

.= (l1 + l2) . v by VECTSP_6:22 ;

:: thesis: verum

end;then not v in Carrier l by TARSKI:def 3, VECTSP_6:def 4;

hence l . v = 0. K

.= (l1 . v) + (0. K) by A4, B1

.= (l1 . v) + (l2 . v) by A8, B1

.= (l1 + l2) . v by VECTSP_6:22 ;

:: thesis: verum