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_{3} being Linear_Combination of R st

for v being Element of R holds b_{3} . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b_{3} being Linear_Combination of R st b_{3} = ZeroLC R ) ) )

hence
( ( r <> 0 implies ex bfor v being Element of R holds

( ( r <> 0 implies ex b

for v being Element of R holds b

deffunc H_{1}( Element of R) -> Element of REAL = LR . ((r ") * $1);

deffunc H_{2}( 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_{1}(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_{3} being Linear_Combination of R st

for v being Element of R holds b_{3} . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b_{3} being Linear_Combination of R st b_{3} = ZeroLC R ) )

{ H_{2}(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_{2} being Linear_Combination of R st

for v being Element of R holds b_{2} . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b_{2} being Linear_Combination of R st b_{2} = ZeroLC R ) )

let v be Element of R; :: thesis: ( ( r <> 0 implies ex b_{1} being Linear_Combination of R st

for v being Element of R holds b_{1} . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b_{1} being Linear_Combination of R st b_{1} = ZeroLC R ) )

f . v = LR . ((r ") * v) by A1;

hence ( ( r <> 0 implies ex b_{1} being Linear_Combination of R st

for v being Element of R holds b_{1} . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b_{1} being Linear_Combination of R st b_{1} = ZeroLC R ) )
by A1; :: thesis: verum

end;deffunc H

consider f being Function of the carrier of R,REAL such that

A1: for v being Element of R holds f . v = H

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

for v being Element of R holds b

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

not f . v <> 0

A7:
Carrier LR is finite
;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;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

{ H

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

for v being Element of R holds b

let v be Element of R; :: thesis: ( ( r <> 0 implies ex b

for v being Element of R holds b

f . v = LR . ((r ") * v) by A1;

hence ( ( r <> 0 implies ex b

for v being Element of R holds b

for v being Element of R holds b