begin
Lm2:
now for V being RealLinearSpace
for v1, v2 being VECTOR of V
for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )
let V be
RealLinearSpace;
for v1, v2 being VECTOR of V
for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )let v1,
v2 be
VECTOR of
V;
for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )let a,
b be
Real;
( v1 <> v2 implies ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b ) )assume A1:
v1 <> v2
;
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )thus
ex
l being
Linear_Combination of
{v1,v2} st
(
l . v1 = a &
l . v2 = b )
verum
end;
Lm3:
now for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )
let V be
RealLinearSpace;
for v1, v2, v3 being VECTOR of V
for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )let v1,
v2,
v3 be
VECTOR of
V;
for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )let a,
b,
c be
Real;
( v1 <> v2 & v1 <> v3 & v2 <> v3 implies ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c ) )assume that A1:
v1 <> v2
and A2:
v1 <> v3
and A3:
v2 <> v3
;
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )thus
ex
l being
Linear_Combination of
{v1,v2,v3} st
(
l . v1 = a &
l . v2 = b &
l . v3 = c )
verum
proof
deffunc H1(
VECTOR of
V)
-> Element of
NAT =
0 ;
consider f being
Function of the
carrier of
V,
REAL such that A4:
(
f . v1 = a &
f . v2 = b &
f . v3 = c )
and A5:
for
u being
VECTOR of
V st
u <> v1 &
u <> v2 &
u <> v3 holds
f . u = H1(
u)
from RLVECT_4:sch 1(A1, A2, A3);
reconsider f =
f as
Element of
Funcs ( the
carrier of
V,
REAL)
by FUNCT_2:8;
then reconsider f =
f as
Linear_Combination of
V by RLVECT_2:def 3;
Carrier f c= {v1,v2,v3}
proof
let x be
set ;
TARSKI:def 3 ( not x in Carrier f or x in {v1,v2,v3} )
assume that A8:
x in Carrier f
and A9:
not
x in {v1,v2,v3}
;
contradiction
A10:
(
x <> v2 &
x <> v3 )
by A9, ENUMSET1:def 1;
(
f . x <> 0 &
x <> v1 )
by A8, A9, ENUMSET1:def 1, RLVECT_2:19;
hence
contradiction
by A5, A8, A10;
verum
end;
then reconsider f =
f as
Linear_Combination of
{v1,v2,v3} by RLVECT_2:def 6;
take
f
;
( f . v1 = a & f . v2 = b & f . v3 = c )
thus
(
f . v1 = a &
f . v2 = b &
f . v3 = c )
by A4;
verum
end;
end;