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