now :: thesis: ( r <> 0 implies ex f being Linear_Combination of R st
for v being Element of R holds
( ( r <> 0 implies ex b3 being Linear_Combination of R st
for v being Element of R holds b3 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b3 being Linear_Combination of R st b3 = ZeroLC R ) ) )
deffunc H1( Element of R) -> Element of REAL = LR . ((r ") * $1);
deffunc H2( 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 = H1(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 b3 being Linear_Combination of R st
for v being Element of R holds b3 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b3 being Linear_Combination of R st b3 = 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 ;
{ H2(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 b2 being Linear_Combination of R st
for v being Element of R holds b2 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b2 being Linear_Combination of R st b2 = ZeroLC R ) )
let v be Element of R; :: thesis: ( ( r <> 0 implies ex b1 being Linear_Combination of R st
for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b1 being Linear_Combination of R st b1 = ZeroLC R ) )
f . v = LR . ((r ") * v) by A1;
hence ( ( r <> 0 implies ex b1 being Linear_Combination of R st
for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b1 being Linear_Combination of R st b1 = ZeroLC R ) ) by A1; :: thesis: verum
end;
hence ( ( r <> 0 implies ex b1 being Linear_Combination of R st
for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b1 being Linear_Combination of R st b1 = ZeroLC R ) ) ; :: thesis: verum