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

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