let V be RealLinearSpace; :: thesis: for p, q, u being Element of V st are_Prop p,u & are_Prop u,q holds

are_Prop p,q

let p, q, u 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 and

A4: a <> 0 and

A5: b <> 0 by A1;

consider c, d being Real such that

A6: c * u = d * q and

A7: c <> 0 and

A8: d <> 0 by A2;

b " <> 0 by A5, XCMPLX_1:202;

then (b ") * a <> 0 by A4, XCMPLX_1:6;

then A9: c * ((b ") * a) <> 0 by A7, XCMPLX_1:6;

((b ") * a) * p = (b ") * (b * u) by A3, RLVECT_1:def 7

.= ((b ") * b) * u by RLVECT_1:def 7

.= 1 * u by A5, XCMPLX_0:def 7

.= u by RLVECT_1:def 8 ;

then d * q = (c * ((b ") * a)) * p by A6, RLVECT_1:def 7;

hence are_Prop p,q by A8, A9; :: thesis: verum

are_Prop p,q

let p, q, u 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 and

A4: a <> 0 and

A5: b <> 0 by A1;

consider c, d being Real such that

A6: c * u = d * q and

A7: c <> 0 and

A8: d <> 0 by A2;

b " <> 0 by A5, XCMPLX_1:202;

then (b ") * a <> 0 by A4, XCMPLX_1:6;

then A9: c * ((b ") * a) <> 0 by A7, XCMPLX_1:6;

((b ") * a) * p = (b ") * (b * u) by A3, RLVECT_1:def 7

.= ((b ") * b) * u by RLVECT_1:def 7

.= 1 * u by A5, XCMPLX_0:def 7

.= u by RLVECT_1:def 8 ;

then d * q = (c * ((b ") * a)) * p by A6, RLVECT_1:def 7;

hence are_Prop p,q by A8, A9; :: thesis: verum