let V be RealLinearSpace; :: 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 Real 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 Real 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 Real 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 Real 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 Real 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 Real ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let r be Real; :: thesis: 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 RLSUB_2:11;
defpred S₁[ VECTOR of (X + (Lin {v})), Real] means for x being VECTOR of X
for s being Real st ($1 |-- W1,(Lin {y})) `1 = x & ($1 |-- W1,(Lin {y})) `2 = s * v holds
$2 = (fi . x) + (s * r);

A3: now

let e be Element of (X + (Lin {v})); :: thesis: ex u being Element of REAL st S₁[e,u]
consider x being VECTOR of X, s being Real such that
A4: e |-- W1,(Lin {y}) = [x,(s * v)] by A1, A2, Th28;
take u = (fi . x) + (s * r); :: thesis: S₁[e,u]
thus S₁[e,u] :: thesis: verum

proof

let x' be VECTOR of X; :: thesis: for s being Real st (e |-- W1,(Lin {y})) `1 = x' & (e |-- W1,(Lin {y})) `2 = s * v holds
u = (fi . x') + (s * r)
let t be Real; :: thesis: ( (e |-- W1,(Lin {y})) `1 = x' & (e |-- W1,(Lin {y})) `2 = t * v implies u = (fi . x') + (t * r) )
assume A5: ( (e |-- W1,(Lin {y})) `1 = x' & (e |-- W1,(Lin {y})) `2 = t * v ) ; :: thesis: u = (fi . x') + (t * r)
A6: v <> 0. V by A2, RLSUB_1:25;
s * v = t * v by A4, A5, MCART_1:7;
then t = s by A6, RLVECT_1:51;
hence u = (fi . x') + (t * r) by A4, A5, MCART_1:7; :: thesis: verum

end;

end;

consider f being Function of the carrier of (X + (Lin {v})),REAL such that
A7: for e being VECTOR of (X + (Lin {v})) holds S₁[e,f . e] from FUNCT_2:sch 3(A3);
A8: dom fi = the carrier of X by FUNCT_2:def 1;

A9: now

let a be set ; :: 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 by FUNCT_2:def 1;
the carrier of X c= the carrier of (X + (Lin {v})) by Th14;
then reconsider v1 = x as VECTOR of (X + (Lin {v})) by TARSKI:def 3;
v1 in X by STRUCT_0:def 5;
then v1 |-- W1,(Lin {y}) = [v1,(0. V)] by A1, A2, Th26
.= [v1,(0 * v)] by RLVECT_1:23 ;
then A10: ( (v1 |-- W1,(Lin {y})) `1 = x & (v1 |-- W1,(Lin {y})) `2 = 0 * v ) by MCART_1:7;
thus fi . a = (fi . x) + (0 * r)
.= f . a by A7, A10 ; :: thesis: verum

end;

reconsider f = f as Functional of (X + (Lin {v})) ;
A11: f is additive

proof

let v1, v2 be VECTOR of (X + (Lin {v})); :: according to HAHNBAN:def 4 :: thesis: f . (v1 + v2) = (f . v1) + (f . v2)
consider x1 being VECTOR of X, s1 being Real such that
A12: v1 |-- W1,(Lin {y}) = [x1,(s1 * v)] by A1, A2, Th28;
consider x2 being VECTOR of X, s2 being Real such that
A13: v2 |-- W1,(Lin {y}) = [x2,(s2 * v)] by A1, A2, Th28;
A14: ( (v1 |-- W1,(Lin {y})) `1 = x1 & (v1 |-- W1,(Lin {y})) `2 = s1 * v ) by A12, MCART_1:7;
A15: ( (v2 |-- W1,(Lin {y})) `1 = x2 & (v2 |-- W1,(Lin {y})) `2 = s2 * v ) by A13, MCART_1:7;
(v1 + v2) |-- W1,(Lin {y}) = [(x1 + x2),((s1 + s2) * v)] by A1, A2, A12, A13, Th29;
then ( ((v1 + v2) |-- W1,(Lin {y})) `1 = x1 + x2 & ((v1 + v2) |-- W1,(Lin {y})) `2 = (s1 + s2) * v ) by MCART_1:7;
hence f . (v1 + v2) = (fi . (x1 + x2)) + ((s1 + s2) * r) by A7
.= ((fi . x1) + (fi . x2)) + ((s1 * r) + (s2 * r)) by Def4
.= ((fi . x1) + (s1 * r)) + ((fi . x2) + (s2 * r))
.= (f . v1) + ((fi . x2) + (s2 * r)) by A7, A14
.= (f . v1) + (f . v2) by A7, A15 ;
:: thesis: verum

end;

f is homogeneous

proof

let v0 be VECTOR of (X + (Lin {v})); :: according to HAHNBAN:def 5 :: thesis: for r being Real holds f . (r * v0) = r * (f . v0)
let t be Real; :: thesis: f . (t * v0) = t * (f . v0)
consider x0 being VECTOR of X, s0 being Real such that
A16: v0 |-- W1,(Lin {y}) = [x0,(s0 * v)] by A1, A2, Th28;
A17: ( (v0 |-- W1,(Lin {y})) `1 = x0 & (v0 |-- W1,(Lin {y})) `2 = s0 * v ) by A16, MCART_1:7;
(t * v0) |-- W1,(Lin {y}) = [(t * x0),((t * s0) * v)] by A1, A2, A16, Th30;
then ( ((t * v0) |-- W1,(Lin {y})) `1 = t * x0 & ((t * v0) |-- W1,(Lin {y})) `2 = (t * s0) * v ) by MCART_1:7;
hence f . (t * v0) = (fi . (t * x0)) + ((t * s0) * r) by A7
.= (t * (fi . x0)) + (t * (s0 * r)) by Def5
.= t * ((fi . x0) + (s0 * r))
.= t * (f . v0) by A7, A17 ;
:: thesis: verum

end;

then reconsider f = f as linear-Functional of (X + (Lin {v})) by A11;
take f ; :: thesis: ( f | the carrier of X = fi & f . y = r )
dom f = the carrier of (X + (Lin {v})) by FUNCT_2:def 1;
then dom fi = (dom f) /\ the carrier of X by A8, Th14, XBOOLE_1:28;
hence f | the carrier of X = fi by A9, FUNCT_1:68; :: thesis: f . y = r
A18: y |-- W1,(Lin {y}) = [(0. W1),y] by A1, A2, Th25;
then A19: (y |-- W1,(Lin {y})) `1 = 0. X by MCART_1:7;
(y |-- W1,(Lin {y})) `2 = y by A18, MCART_1:7
.= 1 * v by A1, RLVECT_1:def 9 ;
hence f . y = (fi . (0. X)) + (1 * r) by A7, A19
.= 0 + (1 * r) by Th33
.= r ;
:: thesis: verum