set V = StructVectSp K;
let x be Vector of (StructVectSp K); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x' = x as Element of K ;
consider t being Element of K such that
A1: x' + t = 0. K by ALGSTR_0:def 11;
reconsider t' = t as Vector of (StructVectSp K) ;
take t' ; :: according to ALGSTR_0:def 11 :: thesis: x + t' = 0. (StructVectSp K)
thus x + t' = 0. (StructVectSp K) by A1; :: thesis: verum