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})) st w in X holds
w |-- W,(Lin {y}) = [w,(0. 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})) st w in X holds
w |-- W,(Lin {y}) = [w,(0. 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})) st w in X holds
w |-- W,(Lin {y}) = [w,(0. 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})) st w in X holds
w |-- W,(Lin {y}) = [w,(0. 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})) st w in X holds
w |-- W,(Lin {y}) = [w,(0. 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})) st w in X holds
w |-- W,(Lin {y}) = [w,(0. V)] )
assume A1: ( v = y & X = W & not v in X ) ; :: thesis: for w being Vector of (X + (Lin {v})) st w in X holds
w |-- W,(Lin {y}) = [w,(0. V)]
let w be Vector of (X + (Lin {v})); :: thesis: ( w in X implies w |-- W,(Lin {y}) = [w,(0. V)] )
assume A2: w in X ; :: thesis: w |-- W,(Lin {y}) = [w,(0. V)]
X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, Th15;
then w |-- W,(Lin {y}) = [w,(0. (X + (Lin {v})))] by A1, A2, Th10;
hence w |-- W,(Lin {y}) = [w,(0. V)] by VECTSP_4:19; :: thesis: verum