let F be Field; :: thesis: for U being VectSp of F
for B being linearly-independent Subset of U
for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
( Carrier l = {w} & l . w = 1. F )
let U be VectSp of F; :: thesis: for B being linearly-independent Subset of U
for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
( Carrier l = {w} & l . w = 1. F )
let B be linearly-independent Subset of U; :: thesis: for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
( Carrier l = {w} & l . w = 1. F )
let w be Element of U; :: thesis: ( w in B implies for l being Linear_Combination of B st Sum l = w holds
( Carrier l = {w} & l . w = 1. F ) )
assume AS1: w in B ; :: thesis: for l being Linear_Combination of B st Sum l = w holds
( Carrier l = {w} & l . w = 1. F )
let l be Linear_Combination of B; :: thesis: ( Sum l = w implies ( Carrier l = {w} & l . w = 1. F ) )
assume AS2: Sum l = w ; :: thesis: ( Carrier l = {w} & l . w = 1. F )
defpred S₁[ object , object ] means ( ( $1 = w & $2 = 1. F ) or ( $1 <> w & $2 = 0. F ) );
B4: for x being object st x in the carrier of U holds
ex y being object st
( y in the carrier of F & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of U implies ex y being object st
( y in the carrier of F & S₁[x,y] ) )
assume x in the carrier of U ; :: thesis: ex y being object st
( y in the carrier of F & S₁[x,y] )

per cases ( x = w or x <> w ) ;

suppose x = w ; :: thesis: ex y being object st
( y in the carrier of F & S₁[x,y] )

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

end;

suppose x <> w ; :: thesis: ex y being object st
( y in the carrier of F & S₁[x,y] )

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

end;

end;

end;

consider l1 being Function of the carrier of U, the carrier of F such that
B5: for x being object st x in the carrier of U holds
S₁[x,l1 . x] from FUNCT_2:sch 1(B4);
reconsider l1 = l1 as Element of Funcs ( the carrier of U, the carrier of F) by FUNCT_2:8;
for v being Element of U st not v in {w} holds
l1 . v = 0. F

proof

let v be Element of U; :: thesis: ( not v in {w} implies l1 . v = 0. F )
assume not v in {w} ; :: thesis: l1 . v = 0. F
then v <> w by TARSKI:def 1;
hence l1 . v = 0. F by B5; :: thesis: verum

end;

then reconsider l1 = l1 as Linear_Combination of U by VECTSP_6:def 1;

now :: thesis: for o being object st o in Carrier l1 holds
o in {w}

let o be object ; :: thesis: ( o in Carrier l1 implies o in {w} )
assume o in Carrier l1 ; :: thesis: o in {w}
then consider v being Element of U such that
C1: ( o = v & l1 . v <> 0. F ) ;
( v = w & l1 . v = 1. F ) by B5, C1;
hence o in {w} by C1, TARSKI:def 1; :: thesis: verum

end;

then B6: Carrier l1 c= {w} ;
then Carrier l1 c= B by AS1, TARSKI:def 1;
then reconsider l1 = l1 as Linear_Combination of B by VECTSP_6:def 4;
B8: Carrier l1 = {w}

proof

now :: thesis: for o being object st o in {w} holds
o in Carrier l1

let o be object ; :: thesis: ( o in {w} implies o in Carrier l1 )
assume C1: o in {w} ; :: thesis: o in Carrier l1
then o = w by TARSKI:def 1;
then l1 . o <> 0. F by B5;
hence o in Carrier l1 by C1; :: thesis: verum

end;

then {w} c= Carrier l1 ;
hence Carrier l1 = {w} by B6; :: thesis: verum

end;

B: l1 . w = 1. F by B5;
Sum l1 = (l1 . w) * w by B8, VECTSP_6:20
.= (1. F) * w by B5
.= w ;
hence ( Carrier l = {w} & l . w = 1. F ) by B8, AS2, B, FIELD_7:6; :: thesis: verum