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 = (Carrier l) \ 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 = (Carrier l) \ 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 = (Carrier l) \ B & ( for x being Element of X st x in Carrier l1 holds

l1 . x = l . x ) )

reconsider T1 = (Carrier l) \ B as finite Subset of X ;

defpred S_{1}[ object , object ] means ( ( $1 in T1 implies $2 = l . $1 ) & ( not $1 in T1 implies $2 = 0 ) );

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

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

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;

then A8: T1 = Carrier l1 by A5;

( T1 c= Carrier l & Carrier l c= A \/ B ) by RLVECT_2:def 6, XBOOLE_1:36;

then ( T1 c= A \/ B & T1 misses B ) by XBOOLE_1:79;

then reconsider l1 = l1 as Linear_Combination of A by A8, RLVECT_2:def 6, XBOOLE_1:73;

take l1 ; :: thesis: ( Carrier l1 = (Carrier l) \ B & ( for x being Element of X st x in Carrier l1 holds

l1 . x = l . x ) )

thus Carrier l1 = (Carrier l) \ 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

for l being Linear_Combination of A \/ B ex l1 being Linear_Combination of A st

( Carrier l1 = (Carrier l) \ 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 = (Carrier l) \ 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 = (Carrier l) \ B & ( for x being Element of X st x in Carrier l1 holds

l1 . x = l . x ) )

reconsider T1 = (Carrier l) \ B as finite Subset of X ;

defpred S

A1: now :: thesis: for x being object st x in the carrier of X holds

ex y being object st

( y in REAL & S_{1}[x,y] )

consider l1 being Function of the carrier of X,REAL such that ex y being object st

( y in REAL & S

let x be object ; :: thesis: ( x in the carrier of X implies ex y being object st

( y in REAL & S_{1}[x,y] ) )

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

( y in REAL & S_{1}[x,y] )

thus ex y being object st

( y in REAL & S_{1}[x,y] )
:: thesis: verum

end;( y in REAL & S

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

( y in REAL & S

thus ex y being object st

( y in REAL & S

proof
end;

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

end;

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

( y in REAL & S_{1}[x,y] )

( y in REAL & S

take y = l . x; :: thesis: ( y in REAL & S_{1}[x,y] )

thus ( y in REAL & S_{1}[x,y] )
by A2, FUNCT_2:5; :: thesis: verum

end;thus ( y in REAL & S

suppose A3:
not x in T1
; :: thesis: ex y being object st

( y in REAL & S_{1}[x,y] )

( y in REAL & S

take y = 0 ; :: thesis: ( y in REAL & S_{1}[x,y] )

thus ( y in REAL & S_{1}[x,y] )
by A3, XREAL_0:def 1; :: thesis: verum

end;thus ( y in REAL & S

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

S

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

then A5:
Carrier l1 c= T1
;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;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

now :: thesis: for x being object st x in T1 holds

x in Carrier l1

then A7:
T1 c= Carrier l1
;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;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

then A8: T1 = Carrier l1 by A5;

( T1 c= Carrier l & Carrier l c= A \/ B ) by RLVECT_2:def 6, XBOOLE_1:36;

then ( T1 c= A \/ B & T1 misses B ) by XBOOLE_1:79;

then reconsider l1 = l1 as Linear_Combination of A by A8, RLVECT_2:def 6, XBOOLE_1:73;

take l1 ; :: thesis: ( Carrier l1 = (Carrier l) \ B & ( for x being Element of X st x in Carrier l1 holds

l1 . x = l . x ) )

thus Carrier l1 = (Carrier l) \ 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