let V be RealLinearSpace; 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; ( 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
; 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; verum