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 ;
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 in NonZero V & v in NonZero V ) by ;
hence [u,v] in Proportionality_as_EqRel_of V by ; :: 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