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

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 & a <> 0 & b <> 0 ) by Def2;
A3: p = 1 * p by RLVECT_1:def 9
.= ((a " ) * a) * p by A2, XCMPLX_0:def 7
.= (a " ) * (b * q) by A2, RLVECT_1:def 9
.= ((a " ) * b) * q by RLVECT_1:def 9 ;
a " <> 0 by A2, XCMPLX_1:203;
hence ex a being Real st
( a <> 0 & p = a * q ) by A2, A3, XCMPLX_1:6; :: thesis: verum

end;

now

given a being Real such that A4: ( a <> 0 & p = a * q ) ; :: thesis: are_Prop p,q
1 * p = a * q by A4, RLVECT_1:def 9;
hence are_Prop p,q by A4, Def2; :: thesis: verum

end;

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