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;

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 ) )

A9:
p <> 0. V
by A3;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;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

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

hence
( a1 = a2 & b1 = b2 )
by A1, A5, A7; :: thesis: verumassume 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;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