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

( a <> 0 & p = a * q ) ) by A1; :: thesis: verum

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

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

now :: thesis: ( ex a being Real st

( a <> 0 & p = a * q ) implies are_Prop p,q )

hence
( are_Prop p,q iff 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;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

( a <> 0 & p = a * q ) ) by A1; :: thesis: verum