now :: thesis: ( r <> 0 implies ex f being Linear_Combination of R st
for v being Element of R holds
( ( r <> 0 implies ex b₃ being Linear_Combination of R st
for v being Element of R holds b₃ . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b₃ being Linear_Combination of R st b₃ = ZeroLC R ) ) )

deffunc H₁( Element of R) -> Element of REAL = LR . ((r ") * $1);
deffunc H₂( Element of R) -> Element of the carrier of R = r * $1;
consider f being Function of the carrier of R,REAL such that
A1: for v being Element of R holds f . v = H₁(v) from FUNCT_2:sch 4();
reconsider f = f as Element of Funcs ( the carrier of R,REAL) by FUNCT_2:8;
assume A2: r <> 0 ; :: thesis: ex f being Linear_Combination of R st
for v being Element of R holds
( ( r <> 0 implies ex b₃ being Linear_Combination of R st
for v being Element of R holds b₃ . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b₃ being Linear_Combination of R st b₃ = ZeroLC R ) )

A3: now :: thesis: for v being Element of R st not v in r * (Carrier LR) holds
not f . v <> 0

let v be Element of R; :: thesis: ( not v in r * (Carrier LR) implies not f . v <> 0 )
assume A4: not v in r * (Carrier LR) ; :: thesis: not f . v <> 0
A5: f . v = LR . ((r ") * v) by A1;
A6: r * ((r ") * v) = (r * (r ")) * v by RLVECT_1:def 7
.= 1 * v by A2, XCMPLX_0:def 7
.= v by RLVECT_1:def 8 ;
assume f . v <> 0 ; :: thesis: contradiction
then (r ") * v in Carrier LR by A5;
hence contradiction by A4, A6; :: thesis: verum

end;

A7: Carrier LR is finite ;
{ H₂(w) where w is Element of R : w in Carrier LR } is finite from FRAENKEL:sch 21(A7);
then reconsider f = f as Linear_Combination of R by A3, RLVECT_2:def 3;
take f = f; :: thesis: for v being Element of R holds
( ( r <> 0 implies ex b₂ being Linear_Combination of R st
for v being Element of R holds b₂ . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b₂ being Linear_Combination of R st b₂ = ZeroLC R ) )
let v be Element of R; :: thesis: ( ( r <> 0 implies ex b₁ being Linear_Combination of R st
for v being Element of R holds b₁ . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b₁ being Linear_Combination of R st b₁ = ZeroLC R ) )
f . v = LR . ((r ") * v) by A1;
hence ( ( r <> 0 implies ex b₁ being Linear_Combination of R st
for v being Element of R holds b₁ . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b₁ being Linear_Combination of R st b₁ = ZeroLC R ) ) by A1; :: thesis: verum

end;

hence ( ( r <> 0 implies ex b₁ being Linear_Combination of R st
for v being Element of R holds b₁ . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b₁ being Linear_Combination of R st b₁ = ZeroLC R ) ) ; :: thesis: verum