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})) 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 that
A1: v = y and
A2: X = W and
A3: 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)]
A4: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th24;
let w be VECTOR of (X + (Lin {v})); :: thesis: ( w in X implies w |-- W,(Lin {y}) = [w,(0. V)] )
assume w in X ; :: thesis: w |-- W,(Lin {y}) = [w,(0. V)]
then w |-- W,(Lin {y}) = [w,(0. (X + (Lin {v})))] by A2, A4, Th19;
hence w |-- W,(Lin {y}) = [w,(0. V)] by RLSUB_1:19; :: thesis: verum