let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let v be VECTOR of V; :: thesis: for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let X be Subspace of V; :: thesis: for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let y be VECTOR of (X + (Lin {v})); :: thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let W be Subspace of X + (Lin {v}); :: thesis: ( v = y & X = W & not v in X implies for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; :: thesis: for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
let w be VECTOR of (X + (Lin {v})); :: thesis: ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
consider v1, v2 being VECTOR of (X + (Lin {v})) such that
A4: w |-- (W,(Lin {y})) = [v1,v2] by Th14;
A5: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th11;
then v1 in W by A4, Th4;
then reconsider x = v1 as VECTOR of X by A2;
v2 in Lin {y} by A5, A4, Th4;
then consider r being Real such that
A6: v2 = r * y by RLVECT_4:8;
take x ; :: thesis: ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
take r ; :: thesis: w |-- (W,(Lin {y})) = [x,(r * v)]
thus w |-- (W,(Lin {y})) = [x,(r * v)] by A1, A4, A6, RLSUB_1:14; :: thesis: verum