let X be non empty addLoopStr ; :: thesis: for A, B being Subset of X
for l being Linear_Combination of A \/ B ex l1 being Linear_Combination of A st
( Carrier l1 = () \ B & ( for x being Element of X st x in Carrier l1 holds
l1 . x = l . x ) )

let A, B be Subset of X; :: thesis: for l being Linear_Combination of A \/ B ex l1 being Linear_Combination of A st
( Carrier l1 = () \ B & ( for x being Element of X st x in Carrier l1 holds
l1 . x = l . x ) )

let l be Linear_Combination of A \/ B; :: thesis: ex l1 being Linear_Combination of A st
( Carrier l1 = () \ B & ( for x being Element of X st x in Carrier l1 holds
l1 . x = l . x ) )

reconsider T1 = () \ B as finite Subset of X ;
defpred S1[ object , object ] means ( ( \$1 in T1 implies \$2 = l . \$1 ) & ( not \$1 in T1 implies \$2 = 0 ) );
A1: now :: thesis: for x being object st x in the carrier of X holds
ex y being object st
( y in REAL & S1[x,y] )
let x be object ; :: thesis: ( x in the carrier of X implies ex y being object st
( y in REAL & S1[x,y] ) )

assume x in the carrier of X ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )

thus ex y being object st
( y in REAL & S1[x,y] ) :: thesis: verum
proof
per cases ( x in T1 or not x in T1 ) ;
suppose A2: x in T1 ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )

take y = l . x; :: thesis: ( y in REAL & S1[x,y] )
thus ( y in REAL & S1[x,y] ) by ; :: thesis: verum
end;
suppose A3: not x in T1 ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )

take y = 0 ; :: thesis: ( y in REAL & S1[x,y] )
thus ( y in REAL & S1[x,y] ) by ; :: thesis: verum
end;
end;
end;
end;
consider l1 being Function of the carrier of X,REAL such that
A4: for x being object st x in the carrier of X holds
S1[x,l1 . x] from reconsider l1 = l1 as Element of Funcs ( the carrier of X,REAL) by FUNCT_2:8;
for x being Element of X st not x in T1 holds
l1 . x = 0 by A4;
then reconsider l1 = l1 as Linear_Combination of X by RLVECT_2:def 3;
now :: thesis: for x being object st x in Carrier l1 holds
x in T1
let x be object ; :: thesis: ( x in Carrier l1 implies x in T1 )
assume x in Carrier l1 ; :: thesis: x in T1
then ex v being Element of X st
( x = v & l1 . v <> 0 ) ;
hence x in T1 by A4; :: thesis: verum
end;
then A5: Carrier l1 c= T1 ;
now :: thesis: for x being object st x in T1 holds
x in Carrier l1
let x be object ; :: thesis: ( x in T1 implies x in Carrier l1 )
assume A6: x in T1 ; :: thesis: x in Carrier l1
then x in Carrier l by XBOOLE_0:def 5;
then l . x <> 0 by RLVECT_2:19;
then l1 . x <> 0 by A4, A6;
hence x in Carrier l1 by A6; :: thesis: verum
end;
then A7: T1 c= Carrier l1 ;
then A8: T1 = Carrier l1 by A5;
( T1 c= Carrier l & Carrier l c= A \/ B ) by ;
then ( T1 c= A \/ B & T1 misses B ) by XBOOLE_1:79;
then reconsider l1 = l1 as Linear_Combination of A by ;
take l1 ; :: thesis: ( Carrier l1 = () \ B & ( for x being Element of X st x in Carrier l1 holds
l1 . x = l . x ) )

thus Carrier l1 = () \ B by A5, A7; :: thesis: for x being Element of X st x in Carrier l1 holds
l1 . x = l . x

thus for x being Element of X st x in Carrier l1 holds
l1 . x = l . x by A4, A5; :: thesis: verum