let V be RealLinearSpace; :: thesis: for p being Element of V holds
( are_Prop p, 0. V iff p = 0. V )
let p be Element of V; :: thesis: ( are_Prop p, 0. V iff p = 0. V )

now

assume are_Prop p, 0. V ; :: thesis: p = 0. V
then consider a, b being Real such that
A1: ( a * p = b * (0. V) & a <> 0 & b <> 0 ) by Def2;
0. V = a * p by A1, RLVECT_1:23;
hence p = 0. V by A1, RLVECT_1:24; :: thesis: verum

end;

hence ( are_Prop p, 0. V iff p = 0. V ) ; :: thesis: verum