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 ;
p = 1 * p by RLVECT_1:def 8
.= ((a ") * a) * p by
.= (a ") * (b * q) by
.= ((a ") * b) * q by RLVECT_1:def 7 ;
hence ex a being Real st
( a <> 0 & p = a * q ) by ; :: 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 ;
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