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
y |-- W,(Lin {y}) = [(0. W),y]
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
y |-- W,(Lin {y}) = [(0. W),y]
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
y |-- W,(Lin {y}) = [(0. W),y]
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
y |-- W,(Lin {y}) = [(0. W),y]
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
y |-- W,(Lin {y}) = [(0. W),y]
let W be Subspace of X + (Lin {v}); :: thesis: ( v = y & X = W & not v in X implies y |-- W,(Lin {y}) = [(0. W),y] )
A1: y in {y} by TARSKI:def 1;
assume ( v = y & X = W & not v in X ) ; :: thesis: y |-- W,(Lin {y}) = [(0. W),y]
then X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by Th15;
then y |-- W,(Lin {y}) = [(0. (X + (Lin {v}))),y] by A1, Th11, VECTSP_7:13;
hence y |-- W,(Lin {y}) = [(0. W),y] by VECTSP_4:19; :: thesis: verum