let V be RealLinearSpace; :: thesis: for p, q being Element of V holds
( are_Prop p,q iff ex a being Real st
( a <> 0 & p = a * q ) )
let p, q be Element of V; :: thesis: ( are_Prop p,q iff ex a being Real st
( a <> 0 & p = a * q ) )

A1: now :: thesis: ( are_Prop p,q implies ex a being Real st
( a <> 0 & p = a * q ) )

assume are_Prop p,q ; :: thesis: ex a being Real st
( a <> 0 & p = a * q )
then consider a, b being Real such that
A2: a * p = b * q and
A3: a <> 0 and
A4: b <> 0 ;
A5: a " <> 0 by A3, XCMPLX_1:202;
p = 1 * p by RLVECT_1:def 8
.= ((a ") * a) * p by A3, XCMPLX_0:def 7
.= (a ") * (b * q) by A2, RLVECT_1:def 7
.= ((a ") * b) * q by RLVECT_1:def 7 ;
hence ex a being Real st
( a <> 0 & p = a * q ) by A4, A5, XCMPLX_1:6; :: thesis: verum

end;

now :: thesis: ( ex a being Real st
( a <> 0 & p = a * q ) implies are_Prop p,q )

given a being Real such that A6: a <> 0 and
A7: p = a * q ; :: thesis: are_Prop p,q
1 * p = a * q by A7, RLVECT_1:def 8;
hence are_Prop p,q by A6; :: thesis: verum

end;

hence ( are_Prop p,q iff ex a being Real st
( a <> 0 & p = a * q ) ) by A1; :: thesis: verum