let u, v, w be non zero Element of (TOP-REAL 3); :: thesis: ( |(u,v)| = 0 & are_Prop w,v implies |(u,w)| = 0 )
assume that
A1: |(u,v)| = 0 and
A2: are_Prop w,v ; :: thesis: |(u,w)| = 0
consider a being Real such that
a <> 0 and
A3: w = a * v by A2, ANPROJ_1:1;
reconsider un = u, vn = v as Element of REAL 3 by EUCLID:22;
thus |(u,w)| = |((a * vn),un)| by A3
.= a * |(v,u)| by EUCLID_8:68
.= 0 by A1 ; :: thesis: verum