let V be RealLinearSpace; :: thesis: for u2, w2 being Element of V
for b1 being Real st b1 * u2 = w2 & b1 <> 0 holds
are_Prop u2,w2
let u2, w2 be Element of V; :: thesis: for b1 being Real st b1 * u2 = w2 & b1 <> 0 holds
are_Prop u2,w2
let b1 be Real; :: thesis: ( b1 * u2 = w2 & b1 <> 0 implies are_Prop u2,w2 )
assume A1: ( b1 * u2 = w2 & b1 <> 0 ) ; :: thesis: are_Prop u2,w2
then b1 * u2 = 1 * w2 by RLVECT_1:def 9;
hence are_Prop u2,w2 by A1, ANPROJ_1:def 2; :: thesis: verum