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 ) )

( [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;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

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

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: verumassume 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;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