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 + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) 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 + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) 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 + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) 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 + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

let v be Vector of V; :: thesis: for y being Vector of (X + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

let y be Vector of (X + (Lin {v})); :: thesis: ( v = y & not v in X implies for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) 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 + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

reconsider W1 = X as Subspace of X + (Lin {v}) by VECTSP_5:7;

let r be Element of K; :: thesis: ex psi being linear-Functional of (X + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

defpred S_{1}[ Element of (X + (Lin {v})), Element of K] means for x being Vector of X

for s being Element of K st ($1 |-- (W1,(Lin {y}))) `1 = x & ($1 |-- (W1,(Lin {y}))) `2 = s * v holds

$2 = (fi . x) + (s * r);

A3: for e being Element of (X + (Lin {v})) ex a being Element of K st S_{1}[e,a]

A7: for e being Element of (X + (Lin {v})) holds S_{1}[e,f . e]
from FUNCT_2:sch 3(A3);

A10: y |-- (W1,(Lin {y})) = [(0. W1),y] by A1, A2, Th15;

then A11: (y |-- (W1,(Lin {y}))) `1 = 0. X ;

A12: f is additive

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 + (Lin {v})) & X is Subspace of X + (Lin {v}) ) by FUNCT_2:def 1, VECTSP_5:7;

then dom fi c= dom f by A19, VECTSP_4:def 2;

then dom fi = (dom f) /\ the carrier of X by A19, XBOOLE_1:28;

hence f | the carrier of X = fi by A8, FUNCT_1:46; :: thesis: f . y = r

(y |-- (W1,(Lin {y}))) `2 = y by A10

.= (1_ K) * v by A1, VECTSP_1:def 17 ;

hence f . y = (fi . (0. X)) + ((1_ K) * r) by A7, A11

.= (0. K) + ((1_ K) * r) by HAHNBAN1:def 9

.= (0. K) + r

.= r by RLVECT_1:4 ;

:: thesis: verum

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 + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) 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 + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) 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 + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) 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 + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

let v be Vector of V; :: thesis: for y being Vector of (X + (Lin {v})) st v = y & not v in X holds

for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

let y be Vector of (X + (Lin {v})); :: thesis: ( v = y & not v in X implies for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) 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 + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

reconsider W1 = X as Subspace of X + (Lin {v}) by VECTSP_5:7;

let r be Element of K; :: thesis: ex psi being linear-Functional of (X + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

defpred S

for s being Element of K st ($1 |-- (W1,(Lin {y}))) `1 = x & ($1 |-- (W1,(Lin {y}))) `2 = s * v holds

$2 = (fi . x) + (s * r);

A3: for e being Element of (X + (Lin {v})) ex a being Element of K st S

proof

consider f being Function of the carrier of (X + (Lin {v})), the carrier of K such that
let e be Element of (X + (Lin {v})); :: thesis: ex a being Element of K st S_{1}[e,a]

consider x being Vector of X, s being Element of K such that

A4: e |-- (W1,(Lin {y})) = [x,(s * v)] by A1, A2, Th18;

take (fi . x) + (s * r) ; :: thesis: S_{1}[e,(fi . x) + (s * r)]

let x9 be Vector of X; :: thesis: for s being Element of K st (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = s * v holds

(fi . x) + (s * r) = (fi . x9) + (s * r)

let t be Element of K; :: thesis: ( (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = t * v implies (fi . x) + (s * r) = (fi . x9) + (t * r) )

assume that

A5: (e |-- (W1,(Lin {y}))) `1 = x9 and

A6: (e |-- (W1,(Lin {y}))) `2 = t * v ; :: thesis: (fi . x) + (s * r) = (fi . x9) + (t * r)

v <> 0. V by A2, VECTSP_4:17;

then t = s by A4, A6, Th4;

hence (fi . x) + (s * r) = (fi . x9) + (t * r) by A4, A5; :: thesis: verum

end;consider x being Vector of X, s being Element of K such that

A4: e |-- (W1,(Lin {y})) = [x,(s * v)] by A1, A2, Th18;

take (fi . x) + (s * r) ; :: thesis: S

let x9 be Vector of X; :: thesis: for s being Element of K st (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = s * v holds

(fi . x) + (s * r) = (fi . x9) + (s * r)

let t be Element of K; :: thesis: ( (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = t * v implies (fi . x) + (s * r) = (fi . x9) + (t * r) )

assume that

A5: (e |-- (W1,(Lin {y}))) `1 = x9 and

A6: (e |-- (W1,(Lin {y}))) `2 = t * v ; :: thesis: (fi . x) + (s * r) = (fi . x9) + (t * r)

v <> 0. V by A2, VECTSP_4:17;

then t = s by A4, A6, Th4;

hence (fi . x) + (s * r) = (fi . x9) + (t * r) by A4, A5; :: thesis: verum

A7: for e being Element of (X + (Lin {v})) holds S

A8: now :: thesis: for a being object st a in dom fi holds

fi . a = f . a

reconsider f = f as Functional of (X + (Lin {v})) ;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 + (Lin {v}) by VECTSP_5:7;

then the carrier of X c= the carrier of (X + (Lin {v})) by VECTSP_4:def 2;

then reconsider v1 = x as Vector of (X + (Lin {v})) ;

v1 in X ;

then v1 |-- (W1,(Lin {y})) = [v1,(0. V)] by A1, A2, Th16

.= [v1,((0. K) * v)] by Th1 ;

then A9: ( (v1 |-- (W1,(Lin {y}))) `1 = x & (v1 |-- (W1,(Lin {y}))) `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;assume a in dom fi ; :: thesis: fi . a = f . a

then reconsider x = a as Vector of X ;

X is Subspace of X + (Lin {v}) by VECTSP_5:7;

then the carrier of X c= the carrier of (X + (Lin {v})) by VECTSP_4:def 2;

then reconsider v1 = x as Vector of (X + (Lin {v})) ;

v1 in X ;

then v1 |-- (W1,(Lin {y})) = [v1,(0. V)] by A1, A2, Th16

.= [v1,((0. K) * v)] by Th1 ;

then A9: ( (v1 |-- (W1,(Lin {y}))) `1 = x & (v1 |-- (W1,(Lin {y}))) `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

A10: y |-- (W1,(Lin {y})) = [(0. W1),y] by A1, A2, Th15;

then A11: (y |-- (W1,(Lin {y}))) `1 = 0. X ;

A12: f is additive

proof

f is homogeneous
let v1, v2 be Vector of (X + (Lin {v})); :: 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,(Lin {y})) = [x1,(s1 * v)] by A1, A2, Th18;

A14: ( (v1 |-- (W1,(Lin {y}))) `1 = x1 & (v1 |-- (W1,(Lin {y}))) `2 = s1 * v ) by A13;

consider x2 being Vector of X, s2 being Element of K such that

A15: v2 |-- (W1,(Lin {y})) = [x2,(s2 * v)] by A1, A2, Th18;

A16: ( (v2 |-- (W1,(Lin {y}))) `1 = x2 & (v2 |-- (W1,(Lin {y}))) `2 = s2 * v ) by A15;

(v1 + v2) |-- (W1,(Lin {y})) = [(x1 + x2),((s1 + s2) * v)] by A1, A2, A13, A15, Th19;

then ( ((v1 + v2) |-- (W1,(Lin {y}))) `1 = x1 + x2 & ((v1 + v2) |-- (W1,(Lin {y}))) `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 A7, A14

.= (f . v1) + (f . v2) by A7, A16 ;

:: thesis: verum

end;consider x1 being Vector of X, s1 being Element of K such that

A13: v1 |-- (W1,(Lin {y})) = [x1,(s1 * v)] by A1, A2, Th18;

A14: ( (v1 |-- (W1,(Lin {y}))) `1 = x1 & (v1 |-- (W1,(Lin {y}))) `2 = s1 * v ) by A13;

consider x2 being Vector of X, s2 being Element of K such that

A15: v2 |-- (W1,(Lin {y})) = [x2,(s2 * v)] by A1, A2, Th18;

A16: ( (v2 |-- (W1,(Lin {y}))) `1 = x2 & (v2 |-- (W1,(Lin {y}))) `2 = s2 * v ) by A15;

(v1 + v2) |-- (W1,(Lin {y})) = [(x1 + x2),((s1 + s2) * v)] by A1, A2, A13, A15, Th19;

then ( ((v1 + v2) |-- (W1,(Lin {y}))) `1 = x1 + x2 & ((v1 + v2) |-- (W1,(Lin {y}))) `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 A7, A14

.= (f . v1) + (f . v2) by A7, A16 ;

:: thesis: verum

proof

then reconsider f = f as linear-Functional of (X + (Lin {v})) by A12;
let v0 be Vector of (X + (Lin {v})); :: according to HAHNBAN1:def 8 :: thesis: for b_{1} being Element of the carrier of K holds f . (b_{1} * v0) = b_{1} * (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,(Lin {y})) = [x0,(s0 * v)] by A1, A2, Th18;

A18: ( (v0 |-- (W1,(Lin {y}))) `1 = x0 & (v0 |-- (W1,(Lin {y}))) `2 = s0 * v ) by A17;

(t * v0) |-- (W1,(Lin {y})) = [(t * x0),((t * s0) * v)] by A1, A2, A17, Th20;

then ( ((t * v0) |-- (W1,(Lin {y}))) `1 = t * x0 & ((t * v0) |-- (W1,(Lin {y}))) `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 A7, A18 ;

:: thesis: verum

end;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,(Lin {y})) = [x0,(s0 * v)] by A1, A2, Th18;

A18: ( (v0 |-- (W1,(Lin {y}))) `1 = x0 & (v0 |-- (W1,(Lin {y}))) `2 = s0 * v ) by A17;

(t * v0) |-- (W1,(Lin {y})) = [(t * x0),((t * s0) * v)] by A1, A2, A17, Th20;

then ( ((t * v0) |-- (W1,(Lin {y}))) `1 = t * x0 & ((t * v0) |-- (W1,(Lin {y}))) `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 A7, A18 ;

:: thesis: verum

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 + (Lin {v})) & X is Subspace of X + (Lin {v}) ) by FUNCT_2:def 1, VECTSP_5:7;

then dom fi c= dom f by A19, VECTSP_4:def 2;

then dom fi = (dom f) /\ the carrier of X by A19, XBOOLE_1:28;

hence f | the carrier of X = fi by A8, FUNCT_1:46; :: thesis: f . y = r

(y |-- (W1,(Lin {y}))) `2 = y by A10

.= (1_ K) * v by A1, VECTSP_1:def 17 ;

hence f . y = (fi . (0. X)) + ((1_ K) * r) by A7, A11

.= (0. K) + ((1_ K) * r) by HAHNBAN1:def 9

.= (0. K) + r

.= r by RLVECT_1:4 ;

:: thesis: verum