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₁[ 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₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st
( y in the carrier of K & S₁[x,y] ) )
assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of K & S₁[x,y] )
then reconsider x9 = x as Vector of V ;

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

suppose B1: x in A1 ; :: thesis: ex y being object st
( y in the carrier of K & S₁[x,y] )

l . x9 in the carrier of K ;
hence ex y being object st
( y in the carrier of K & S₁[x,y] ) by B1; :: thesis: verum

end;

suppose not x in A1 ; :: thesis: ex y being object st
( y in the carrier of K & S₁[x,y] )

hence ex y being object st
( y in the carrier of K & S₁[x,y] ) ; :: thesis: verum

end;

end;

end;

ex l1 being Function of the carrier of V, the carrier of K st
for x being object st x in the carrier of V holds
S₁[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₁[x,l1 . x] ;

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

let v be Vector of V; :: thesis: ( not v in A1 /\ (Carrier l) implies l1 . b₁ = 0. K )
assume A6: not v in A1 /\ (Carrier l) ; :: thesis: l1 . b₁ = 0. K

per cases ( not v in A1 or not v in Carrier l ) by A6, XBOOLE_0:def 4;

suppose not v in A1 ; :: thesis: l1 . b₁ = 0. K

hence l1 . v = 0. K by A4; :: thesis: verum

end;

suppose not v in Carrier l ; :: thesis: l1 . b₁ = 0. K

then l . v = 0. K ;
hence l1 . v = 0. K by A4; :: thesis: verum

end;

end;

end;

reconsider l1 = l1 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;
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

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;

then AX1: l1 is Linear_Combination of A1 by TARSKI:def 3, VECTSP_6:def 4;
defpred S₂[ 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₂[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st
( y in the carrier of K & S₂[x,y] ) )
assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of K & S₂[x,y] )
then reconsider x9 = x as Vector of V ;

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

suppose B1: x in A2 ; :: thesis: ex y being object st
( y in the carrier of K & S₂[x,y] )

l . x9 in the carrier of K ;
hence ex y being object st
( y in the carrier of K & S₂[x,y] ) by B1; :: thesis: verum

end;

suppose not x in A2 ; :: thesis: ex y being object st
( y in the carrier of K & S₂[x,y] )

hence ex y being object st
( y in the carrier of K & S₂[x,y] ) ; :: thesis: verum

end;

end;

end;

ex l2 being Function of the carrier of V, the carrier of K st
for x being object st x in the carrier of V holds
S₂[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₂[x,l2 . x] ;

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

let v be Vector of V; :: thesis: ( not v in A2 /\ (Carrier l) implies l2 . b₁ = 0. K )
assume A10: not v in A2 /\ (Carrier l) ; :: thesis: l2 . b₁ = 0. K

per cases ( not v in A2 or not v in Carrier l ) by A10, XBOOLE_0:def 4;

suppose not v in A2 ; :: thesis: l2 . b₁ = 0. K

hence l2 . v = 0. K by A8; :: thesis: verum

end;

suppose not v in Carrier l ; :: thesis: l2 . b₁ = 0. K

then l . v = 0. K ;
hence l2 . v = 0. K by A8; :: thesis: verum

end;

end;

end;

reconsider l2 = l2 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;
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

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;

then AX2: l2 is Linear_Combination of A2 by TARSKI:def 3, VECTSP_6:def 4;
for v being Vector of V holds l . v = (l1 + l2) . v

proof

let v be Vector of V; :: thesis: l . v = (l1 + l2) . v

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

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;

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;

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;

end;

end;

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