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 )
reconsider W1 = X as Subspace of X + (Lin {v}) by RLSUB_2:7;
let r be Real; :: thesis: ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
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 :: thesis: for e being Element of (X + (Lin {v})) ex u being Element of REAL st S₁[e,u]

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, Th15;
reconsider u = (fi . x) + (s * r) as Element of REAL by XREAL_0:def 1;
take u = u; :: thesis: S₁[e,u]
thus S₁[e,u] :: thesis: verum

proof

let x9 be VECTOR of X; :: thesis: for s being Real st (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = s * v holds
u = (fi . x9) + (s * r)
let t be Real; :: thesis: ( (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = t * v implies u = (fi . x9) + (t * r) )
assume that
A5: (e |-- (W1,(Lin {y}))) `1 = x9 and
A6: (e |-- (W1,(Lin {y}))) `2 = t * v ; :: thesis: u = (fi . x9) + (t * r)
v <> 0. V by A2, RLSUB_1:17;
then t = s by A4, A6, RLVECT_1:37;
hence u = (fi . x9) + (t * r) by A4, A5; :: 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: 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 by FUNCT_2:def 1;
the carrier of X c= the carrier of (X + (Lin {v})) by Th1;
then reconsider v1 = x as VECTOR of (X + (Lin {v})) ;
v1 in X ;
then v1 |-- (W1,(Lin {y})) = [v1,(0. V)] by A1, A2, Th13
.= [v1,(0 * v)] by RLVECT_1:10 ;
then A9: ( (v1 |-- (W1,(Lin {y}))) `1 = x & (v1 |-- (W1,(Lin {y}))) `2 = 0 * v ) ;
thus fi . a = (fi . x) + (0 * r)
.= f . a by A7, A9 ; :: thesis: verum

end;

reconsider f = f as Functional of (X + (Lin {v})) ;
A10: y |-- (W1,(Lin {y})) = [(0. W1),y] by A1, A2, Th12;
then A11: (y |-- (W1,(Lin {y}))) `1 = 0. X ;
A12: f is additive

proof

let v1, v2 be VECTOR of (X + (Lin {v})); :: according to HAHNBAN:def 2 :: thesis: f . (v1 + v2) = (f . v1) + (f . v2)
consider x1 being VECTOR of X, s1 being Real such that
A13: v1 |-- (W1,(Lin {y})) = [x1,(s1 * v)] by A1, A2, Th15;
A14: ( (v1 |-- (W1,(Lin {y}))) `1 = x1 & (v1 |-- (W1,(Lin {y}))) `2 = s1 * v ) by A13;
consider x2 being VECTOR of X, s2 being Real such that
A15: v2 |-- (W1,(Lin {y})) = [x2,(s2 * v)] by A1, A2, Th15;
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, Th16;
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) + (fi . x2)) + ((s1 * r) + (s2 * r)) by Def2
.= ((fi . x1) + (s1 * r)) + ((fi . x2) + (s2 * r))
.= (f . v1) + ((fi . x2) + (s2 * r)) by A7, A14
.= (f . v1) + (f . v2) by A7, A16 ;
:: thesis: verum

end;

f is homogeneous

proof

let v0 be VECTOR of (X + (Lin {v})); :: according to HAHNBAN:def 3 :: 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
A17: v0 |-- (W1,(Lin {y})) = [x0,(s0 * v)] by A1, A2, Th15;
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, Th17;
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 Def3
.= t * ((fi . x0) + (s0 * r))
.= t * (f . v0) by A7, A18 ;
:: thesis: verum

end;

then reconsider f = f as linear-Functional of (X + (Lin {v})) by A12;
take f ; :: thesis: ( f | the carrier of X = fi & f . y = r )
( dom fi = the carrier of X & dom f = the carrier of (X + (Lin {v})) ) by FUNCT_2:def 1;
then dom fi = (dom f) /\ the carrier of X by Th1, 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 * v by A1, RLVECT_1:def 8 ;
hence f . y = (fi . (0. X)) + (1 * r) by A7, A11
.= 0 + (1 * r) by Th20
.= r ;
:: thesis: verum