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 that
A1: not are_Prop p,q and
A2: (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) and
A3: not p is zero and
A4: not q is zero ; :: thesis: ( a1 = a2 & b1 = b2 )
((a2 * p) + (b2 * q)) + (- (b1 * q)) = (a1 * p) + ((b1 * q) + (- (b1 * q))) by A2, RLVECT_1:def 3
.= (a1 * p) + (0. V) by RLVECT_1:5
.= a1 * p ;
then a1 * p = ((b2 * q) + (- (b1 * q))) + (a2 * p) by RLVECT_1:def 3
.= ((b2 * q) - (b1 * q)) + (a2 * p) by RLVECT_1:def 11
.= ((b2 - b1) * q) + (a2 * p) by RLVECT_1:35 ;
then (a1 * p) + (- (a2 * p)) = ((b2 - b1) * q) + ((a2 * p) + (- (a2 * p))) by RLVECT_1:def 3
.= ((b2 - b1) * q) + (0. V) by RLVECT_1:5
.= (b2 - b1) * q ;
then A5: (b2 - b1) * q = (a1 * p) - (a2 * p) by RLVECT_1:def 11
.= (a1 - a2) * p by RLVECT_1:35 ;
A6: q <> 0. V by A4;

A7: now :: thesis: ( a1 - a2 = 0 implies ( a1 = a2 & b1 = b2 ) )

assume A8: a1 - a2 = 0 ; :: thesis: ( a1 = a2 & b1 = b2 )
then (b2 - b1) * q = 0. V by A5, RLVECT_1:10;
then b2 - b1 = 0 by A6, RLVECT_1:11;
hence ( a1 = a2 & b1 = b2 ) by A8; :: thesis: verum

end;

A9: p <> 0. V by A3;

now :: thesis: ( b2 - b1 = 0 implies ( a1 = a2 & b1 = b2 ) )

assume A10: b2 - b1 = 0 ; :: thesis: ( a1 = a2 & b1 = b2 )
then (a1 - a2) * p = 0. V by A5, RLVECT_1:10;
then a1 - a2 = 0 by A9, RLVECT_1:11;
hence ( a1 = a2 & b1 = b2 ) by A10; :: thesis: verum

end;

hence ( a1 = a2 & b1 = b2 ) by A1, A5, A7; :: thesis: verum