let V be RealLinearSpace; :: thesis: for u, v being Element of V holds
( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) )
let u, v be Element of V; :: thesis: ( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) )

A1: now :: thesis: ( [u,v] in Proportionality_as_EqRel_of V implies ( not u is zero & not v is zero & are_Prop u,v ) )

assume A2: [u,v] in Proportionality_as_EqRel_of V ; :: thesis: ( not u is zero & not v is zero & are_Prop u,v )
then ( u in NonZero V & v in NonZero V ) by Def3;
hence ( not u is zero & not v is zero ) by STRUCT_0:1; :: thesis: are_Prop u,v
ex u1, v1 being Element of V st
( u = u1 & v = v1 & are_Prop u1,v1 ) by A2, Def3;
hence are_Prop u,v ; :: thesis: verum

end;

now :: thesis: ( not u is zero & not v is zero & are_Prop u,v implies [u,v] in Proportionality_as_EqRel_of V )

assume that
A3: ( not u is zero & not v is zero ) and
A4: are_Prop u,v ; :: thesis: [u,v] in Proportionality_as_EqRel_of V
( u in NonZero V & v in NonZero V ) by A3, STRUCT_0:1;
hence [u,v] in Proportionality_as_EqRel_of V by A4, Def3; :: thesis: verum

end;

hence ( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) ) by A1; :: thesis: verum