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

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