let K be Field; :: thesis: for V being VectSp of K
for X being Subspace of V
for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + ()) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + ()) st
( psi | the carrier of X = fi & psi . y = r )

let V be VectSp of K; :: thesis: for X being Subspace of V
for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + ()) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + ()) st
( psi | the carrier of X = fi & psi . y = r )

let X be Subspace of V; :: thesis: for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + ()) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + ()) st
( psi | the carrier of X = fi & psi . y = r )

let fi be linear-Functional of X; :: thesis: for v being Vector of V
for y being Vector of (X + ()) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + ()) st
( psi | the carrier of X = fi & psi . y = r )

let v be Vector of V; :: thesis: for y being Vector of (X + ()) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + ()) st
( psi | the carrier of X = fi & psi . y = r )

let y be Vector of (X + ()); :: thesis: ( v = y & not v in X implies for r being Element of K ex psi being linear-Functional of (X + ()) st
( psi | the carrier of X = fi & psi . y = r ) )

assume that
A1: v = y and
A2: not v in X ; :: thesis: for r being Element of K ex psi being linear-Functional of (X + ()) st
( psi | the carrier of X = fi & psi . y = r )

reconsider W1 = X as Subspace of X + () by VECTSP_5:7;
let r be Element of K; :: thesis: ex psi being linear-Functional of (X + ()) st
( psi | the carrier of X = fi & psi . y = r )

defpred S1[ Element of (X + ()), Element of K] means for x being Vector of X
for s being Element of K st (\$1 |-- (W1,())) `1 = x & (\$1 |-- (W1,())) `2 = s * v holds
\$2 = (fi . x) + (s * r);
A3: for e being Element of (X + ()) ex a being Element of K st S1[e,a]
proof
let e be Element of (X + ()); :: thesis: ex a being Element of K st S1[e,a]
consider x being Vector of X, s being Element of K such that
A4: e |-- (W1,()) = [x,(s * v)] by A1, A2, Th18;
take (fi . x) + (s * r) ; :: thesis: S1[e,(fi . x) + (s * r)]
let x9 be Vector of X; :: thesis: for s being Element of K st (e |-- (W1,())) `1 = x9 & (e |-- (W1,())) `2 = s * v holds
(fi . x) + (s * r) = (fi . x9) + (s * r)

let t be Element of K; :: thesis: ( (e |-- (W1,())) `1 = x9 & (e |-- (W1,())) `2 = t * v implies (fi . x) + (s * r) = (fi . x9) + (t * r) )
assume that
A5: (e |-- (W1,())) `1 = x9 and
A6: (e |-- (W1,())) `2 = t * v ; :: thesis: (fi . x) + (s * r) = (fi . x9) + (t * r)
v <> 0. V by ;
then t = s by A4, A6, Th4;
hence (fi . x) + (s * r) = (fi . x9) + (t * r) by A4, A5; :: thesis: verum
end;
consider f being Function of the carrier of (X + ()), the carrier of K such that
A7: for e being Element of (X + ()) holds S1[e,f . e] from
A8: now :: thesis: for a being object st a in dom fi holds
fi . a = f . a
let a be object ; :: thesis: ( a in dom fi implies fi . a = f . a )
assume a in dom fi ; :: thesis: fi . a = f . a
then reconsider x = a as Vector of X ;
X is Subspace of X + () by VECTSP_5:7;
then the carrier of X c= the carrier of (X + ()) by VECTSP_4:def 2;
then reconsider v1 = x as Vector of (X + ()) ;
v1 in X ;
then v1 |-- (W1,()) = [v1,(0. V)] by A1, A2, Th16
.= [v1,((0. K) * v)] by Th1 ;
then A9: ( (v1 |-- (W1,())) `1 = x & (v1 |-- (W1,())) `2 = (0. K) * v ) ;
thus fi . a = (fi . x) + (0. K) by RLVECT_1:4
.= (fi . x) + ((0. K) * r)
.= f . a by A7, A9 ; :: thesis: verum
end;
reconsider f = f as Functional of (X + ()) ;
A10: y |-- (W1,()) = [(0. W1),y] by A1, A2, Th15;
then A11: (y |-- (W1,())) `1 = 0. X ;
proof
let v1, v2 be Vector of (X + ()); :: according to VECTSP_1:def 19 :: thesis: f . (v1 + v2) = (f . v1) + (f . v2)
consider x1 being Vector of X, s1 being Element of K such that
A13: v1 |-- (W1,()) = [x1,(s1 * v)] by A1, A2, Th18;
A14: ( (v1 |-- (W1,())) `1 = x1 & (v1 |-- (W1,())) `2 = s1 * v ) by A13;
consider x2 being Vector of X, s2 being Element of K such that
A15: v2 |-- (W1,()) = [x2,(s2 * v)] by A1, A2, Th18;
A16: ( (v2 |-- (W1,())) `1 = x2 & (v2 |-- (W1,())) `2 = s2 * v ) by A15;
(v1 + v2) |-- (W1,()) = [(x1 + x2),((s1 + s2) * v)] by A1, A2, A13, A15, Th19;
then ( ((v1 + v2) |-- (W1,())) `1 = x1 + x2 & ((v1 + v2) |-- (W1,())) `2 = (s1 + s2) * v ) ;
hence f . (v1 + v2) = (fi . (x1 + x2)) + ((s1 + s2) * r) by A7
.= (fi . (x1 + x2)) + ((s1 * r) + (s2 * r)) by VECTSP_1:def 3
.= ((fi . x1) + (fi . x2)) + ((s1 * r) + (s2 * r)) by VECTSP_1:def 20
.= (((fi . x1) + (fi . x2)) + (s1 * r)) + (s2 * r) by RLVECT_1:def 3
.= (((fi . x1) + (s1 * r)) + (fi . x2)) + (s2 * r) by RLVECT_1:def 3
.= ((fi . x1) + (s1 * r)) + ((fi . x2) + (s2 * r)) by RLVECT_1:def 3
.= (f . v1) + ((fi . x2) + (s2 * r)) by
.= (f . v1) + (f . v2) by ;
:: thesis: verum
end;
f is homogeneous
proof
let v0 be Vector of (X + ()); :: according to HAHNBAN1:def 8 :: thesis: for b1 being Element of the carrier of K holds f . (b1 * v0) = b1 * (f . v0)
let t be Element of K; :: thesis: f . (t * v0) = t * (f . v0)
consider x0 being Vector of X, s0 being Element of K such that
A17: v0 |-- (W1,()) = [x0,(s0 * v)] by A1, A2, Th18;
A18: ( (v0 |-- (W1,())) `1 = x0 & (v0 |-- (W1,())) `2 = s0 * v ) by A17;
(t * v0) |-- (W1,()) = [(t * x0),((t * s0) * v)] by A1, A2, A17, Th20;
then ( ((t * v0) |-- (W1,())) `1 = t * x0 & ((t * v0) |-- (W1,())) `2 = (t * s0) * v ) ;
hence f . (t * v0) = (fi . (t * x0)) + ((t * s0) * r) by A7
.= (t * (fi . x0)) + ((t * s0) * r) by HAHNBAN1:def 8
.= (t * (fi . x0)) + (t * (s0 * r)) by GROUP_1:def 3
.= t * ((fi . x0) + (s0 * r)) by VECTSP_1:def 2
.= t * (f . v0) by ;
:: thesis: verum
end;
then reconsider f = f as linear-Functional of (X + ()) by A12;
take f ; :: thesis: ( f | the carrier of X = fi & f . y = r )
A19: dom fi = the carrier of X by FUNCT_2:def 1;
( dom f = the carrier of (X + ()) & X is Subspace of X + () ) by ;
then dom fi c= dom f by ;
then dom fi = (dom f) /\ the carrier of X by ;
hence f | the carrier of X = fi by ; :: thesis: f . y = r
(y |-- (W1,())) `2 = y by A10
.= (1_ K) * v by ;
hence f . y = (fi . (0. X)) + ((1_ K) * r) by
.= (0. K) + ((1_ K) * r) by HAHNBAN1:def 9
.= (0. K) + r
.= r by RLVECT_1:4 ;
:: thesis: verum