let K be Ring; :: thesis:
let V be VectSp of K; :: thesis:
let A1, A2 be Subset of V; :: thesis:
let l be Linear_Combination of A1 \/ A2; :: thesis:
assume A1: A1 /\ A2 = {} ; :: thesis:
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:
assume x in the carrier of V ; :: thesis:
then reconsider x9 = x as Vector of V ;

per cases ;

suppose B1: x in A1 ; :: thesis:

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:

end;

suppose not x in A1 ; :: thesis:

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

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:

let v be Vector of V; :: thesis:
assume A6: not v in A1 /\ (Carrier l) ; :: thesis:

per cases by A6, XBOOLE_0:def 4;

suppose not v in A1 ; :: thesis:

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

end;

suppose not v in Carrier l ; :: thesis:

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

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:
assume B1: x in Carrier l1 ; :: thesis:
then reconsider x = x as Vector of V ;
l1 . x <> 0. K by B1, VECTSP_6:2;
hence x in A1 by A4; :: thesis:

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:
assume x in the carrier of V ; :: thesis:
then reconsider x9 = x as Vector of V ;

per cases ;

suppose B1: x in A2 ; :: thesis:

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:

end;

suppose not x in A2 ; :: thesis:

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

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:

let v be Vector of V; :: thesis:
assume A10: not v in A2 /\ (Carrier l) ; :: thesis:

per cases by A10, XBOOLE_0:def 4;

suppose not v in A2 ; :: thesis:

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

end;

suppose not v in Carrier l ; :: thesis:

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

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:
assume B1: x in Carrier l2 ; :: thesis:
then reconsider x = x as Vector of V ;
l2 . x <> 0. K by B1, VECTSP_6:2;
hence x in A2 by A8; :: thesis:

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:

per cases ;

suppose B1: v in A1 ; :: thesis:

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:

end;

suppose B1: v in A2 ; :: thesis:

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:

end;

suppose B1: ( not v in A1 & not v in A2 ) ; :: thesis:

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:

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: