let V be RealLinearSpace; for p, q, y being Element of V
for a being Real st not are_Prop p,q & y = a * q & a <> 0 holds
not are_Prop p,y
let p, q, y be Element of V; for a being Real st not are_Prop p,q & y = a * q & a <> 0 holds
not are_Prop p,y
let a be Real; ( not are_Prop p,q & y = a * q & a <> 0 implies not are_Prop p,y )
assume that
A1:
not are_Prop p,q
and
A2:
( y = a * q & a <> 0 )
; not are_Prop p,y
assume
are_Prop p,y
; contradiction
then consider b being Real such that
A3:
( b <> 0 & p = b * y )
by ANPROJ_1:1;
( p = (b * a) * q & b * a <> 0 )
by A2, A3, RLVECT_1:def 7, XCMPLX_1:6;
hence
contradiction
by A1, ANPROJ_1:1; verum