let K be Field; 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; 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; 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; 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})); 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}); ( v = y & X = W & not v in X implies y |-- (W,(Lin {y})) = [(0. W),y] )
assume
( v = y & X = W & not v in X )
; y |-- (W,(Lin {y})) = [(0. W),y]
then
( y in {y} & X + (Lin {v}) is_the_direct_sum_of W, Lin {y} )
by Th14, TARSKI:def 1;
then
y |-- (W,(Lin {y})) = [(0. (X + (Lin {v}))),y]
by Th10, VECTSP_7:8;
hence
y |-- (W,(Lin {y})) = [(0. W),y]
by VECTSP_4:11; verum