let V be RealUnitarySpace; for w1, w2 being VECTOR of V
for x being set holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
let w1, w2 be VECTOR of V; for x being set holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
let x be set ; ( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
thus
( x in Lin {w1,w2} implies ex a, b being Real st x = (a * w1) + (b * w2) )
( ex a, b being Real st x = (a * w1) + (b * w2) implies x in Lin {w1,w2} )proof
assume A1:
x in Lin {w1,w2}
;
ex a, b being Real st x = (a * w1) + (b * w2)
hence
ex
a,
b being
Real st
x = (a * w1) + (b * w2)
;
verum
end;
given a, b being Real such that A5:
x = (a * w1) + (b * w2)
; x in Lin {w1,w2}
now x in Lin {w1,w2}per cases
( w1 = w2 or w1 <> w2 )
;
suppose A7:
w1 <> w2
;
x in Lin {w1,w2}deffunc H1(
set )
-> Element of
REAL =
In (
0,
REAL);
reconsider a =
a,
b =
b as
Element of
REAL by XREAL_0:def 1;
consider f being
Function of the
carrier of
V,
REAL such that A8:
(
f . w1 = a &
f . w2 = b )
and A9:
for
u being
VECTOR of
V st
u <> w1 &
u <> w2 holds
f . u = H1(
u)
from FUNCT_2:sch 7(A7);
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= {w1,w2}
then reconsider f =
f as
Linear_Combination of
{w1,w2} by RLVECT_2:def 6;
x = Sum f
by A5, A7, A8, RLVECT_2:33;
hence
x in Lin {w1,w2}
by Th1;
verum end; end; end;
hence
x in Lin {w1,w2}
; verum