let V be RealLinearSpace; :: thesis: for p, q being Element of V
for a1, b1, a2, b2 being Real st not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero holds
( a1 = a2 & b1 = b2 )
let p, q be Element of V; :: thesis: for a1, b1, a2, b2 being Real st not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero holds
( a1 = a2 & b1 = b2 )
let a1, b1, a2, b2 be Real; :: thesis: ( not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero implies ( a1 = a2 & b1 = b2 ) )
assume A1: ( not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero ) ; :: thesis: ( a1 = a2 & b1 = b2 )
then A2: ( p <> 0. V & q <> 0. V ) by STRUCT_0:def 15;
A3: (a1 - a2) * p = (b2 - b1) * q

proof

((a2 * p) + (b2 * q)) + (- (b1 * q)) = (a1 * p) + ((b1 * q) + (- (b1 * q))) by A1, RLVECT_1:def 6
.= (a1 * p) + (0. V) by RLVECT_1:16
.= a1 * p by RLVECT_1:10 ;
then a1 * p = ((b2 * q) + (- (b1 * q))) + (a2 * p) by RLVECT_1:def 6
.= ((b2 * q) - (b1 * q)) + (a2 * p) by RLVECT_1:def 12
.= ((b2 - b1) * q) + (a2 * p) by RLVECT_1:49 ;
then (a1 * p) + (- (a2 * p)) = ((b2 - b1) * q) + ((a2 * p) + (- (a2 * p))) by RLVECT_1:def 6
.= ((b2 - b1) * q) + (0. V) by RLVECT_1:16
.= (b2 - b1) * q by RLVECT_1:10 ;
hence (b2 - b1) * q = (a1 * p) - (a2 * p) by RLVECT_1:def 12
.= (a1 - a2) * p by RLVECT_1:49 ;
:: thesis: verum

end;

A4: now

assume A5: a1 - a2 = 0 ; :: thesis: ( a1 = a2 & b1 = b2 )
then (b2 - b1) * q = 0. V by A3, RLVECT_1:23;
then b2 - b1 = 0 by A2, RLVECT_1:24;
hence ( a1 = a2 & b1 = b2 ) by A5; :: thesis: verum

end;

now

assume A6: b2 - b1 = 0 ; :: thesis: ( a1 = a2 & b1 = b2 )
then (a1 - a2) * p = 0. V by A3, RLVECT_1:23;
then a1 - a2 = 0 by A2, RLVECT_1:24;
hence ( a1 = a2 & b1 = b2 ) by A6; :: thesis: verum

end;

hence ( a1 = a2 & b1 = b2 ) by A1, A3, A4, Def2; :: thesis: verum