let V be RealLinearSpace; :: thesis: for p, u, q being Element of V st are_Prop p,u & are_Prop u,q holds
are_Prop p,q
let p, u, q be Element of V; :: thesis: ( are_Prop p,u & are_Prop u,q implies are_Prop p,q )
assume that
A1: are_Prop p,u and
A2: are_Prop u,q ; :: thesis: are_Prop p,q
consider a, b being Real such that
A3: ( a * p = b * u & a <> 0 & b <> 0 ) by A1, Def2;
consider c, d being Real such that
A4: ( c * u = d * q & c <> 0 & d <> 0 ) by A2, Def2;
((b " ) * a) * p = (b " ) * (b * u) by A3, RLVECT_1:def 9
.= ((b " ) * b) * u by RLVECT_1:def 9
.= 1 * u by A3, XCMPLX_0:def 7
.= u by RLVECT_1:def 9 ;
then A5: d * q = (c * ((b " ) * a)) * p by A4, RLVECT_1:def 9;
b " <> 0 by A3, XCMPLX_1:203;
then (b " ) * a <> 0 by A3, XCMPLX_1:6;
then c * ((b " ) * a) <> 0 by A4, XCMPLX_1:6;
hence are_Prop p,q by A4, A5, Def2; :: thesis: verum