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 that
A1: b1 * u2 = w2 and
A2: b1 <> 0 ; :: thesis: are_Prop u2,w2
b1 * u2 = 1 * w2 by A1, RLVECT_1:def 8;
hence are_Prop u2,w2 by A2; :: thesis: verum