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

assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of K & S1[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 & S1[x,y] )

l . x9 in the carrier of K ;
hence ex y being object st
( y in the carrier of K & S1[x,y] ) by B1; :: thesis: verum
end;
suppose not x in A1 ; :: thesis: ex y being object st
( y in the carrier of K & S1[x,y] )

hence ex y being object st
( y in the carrier of K & S1[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
S1[x,l1 . x] from 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
S1[x,l1 . x] ;
A5: now :: thesis: for v being Vector of V st not v in A1 /\ () holds
l1 . v = 0. K
let v be Vector of V; :: thesis: ( not v in A1 /\ () implies l1 . b1 = 0. K )
assume A6: not v in A1 /\ () ; :: thesis: l1 . b1 = 0. K
per cases ( not v in A1 or not v in Carrier l ) by ;
suppose not v in A1 ; :: thesis: l1 . b1 = 0. K
hence l1 . v = 0. K by A4; :: thesis: verum
end;
suppose not v in Carrier l ; :: thesis: l1 . b1 = 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 ;
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 ;
hence x in A1 by A4; :: thesis: verum
end;
then AX1: l1 is Linear_Combination of A1 by ;
defpred S2[ 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 & S2[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 & S2[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of K & S2[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 & S2[x,y] )

l . x9 in the carrier of K ;
hence ex y being object st
( y in the carrier of K & S2[x,y] ) by B1; :: thesis: verum
end;
suppose not x in A2 ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )

hence ex y being object st
( y in the carrier of K & S2[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
S2[x,l2 . x] from 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
S2[x,l2 . x] ;
A9: now :: thesis: for v being Vector of V st not v in A2 /\ () holds
l2 . v = 0. K
let v be Vector of V; :: thesis: ( not v in A2 /\ () implies l2 . b1 = 0. K )
assume A10: not v in A2 /\ () ; :: thesis: l2 . b1 = 0. K
per cases ( not v in A2 or not v in Carrier l ) by ;
suppose not v in A2 ; :: thesis: l2 . b1 = 0. K
hence l2 . v = 0. K by A8; :: thesis: verum
end;
suppose not v in Carrier l ; :: thesis: l2 . b1 = 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 ;
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 ;
hence x in A2 by A8; :: thesis: verum
end;
then AX2: l2 is Linear_Combination of A2 by ;
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 ;
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 ;
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 ;
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 ; :: thesis: verum