let K be Field; :: thesis: for V being VectSp of K

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 Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]

let V be VectSp of K; :: 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 Element of K 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 Element of K 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 Element of K 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 Element of K 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 Element of K 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 Element of K 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 Element of K 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 Th17;

A5: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th14;

then v1 in W by A4, Th7;

then reconsider x = v1 as Vector of X by A2;

v2 in Lin {y} by A5, A4, Th7;

then consider r being Element of K such that

A6: v2 = r * y by Th3;

take x ; :: thesis: ex r being Element of K 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, VECTSP_4:14; :: thesis: verum

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 Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]

let V be VectSp of K; :: 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 Element of K 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 Element of K 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 Element of K 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 Element of K 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 Element of K 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 Element of K 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 Element of K 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 Th17;

A5: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th14;

then v1 in W by A4, Th7;

then reconsider x = v1 as Vector of X by A2;

v2 in Lin {y} by A5, A4, Th7;

then consider r being Element of K such that

A6: v2 = r * y by Th3;

take x ; :: thesis: ex r being Element of K 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, VECTSP_4:14; :: thesis: verum