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