let a1, a2, b1, b2 be Real; :: thesis: for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 & (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) holds
( a1 = b1 & a2 = b2 )
let n be Nat; :: thesis: for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 & (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) holds
( a1 = b1 & a2 = b2 )
let x1, x2 be Element of REAL n; :: thesis: ( x1,x2 are_lindependent2 & (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) implies ( a1 = b1 & a2 = b2 ) )
assume A1: x1,x2 are_lindependent2 ; :: thesis: ( not (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) or ( a1 = b1 & a2 = b2 ) )
assume A2: (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) ; :: thesis: ( a1 = b1 & a2 = b2 )
0* n = ((a1 * x1) + (a2 * x2)) - ((a1 * x1) + (a2 * x2)) by Th2
.= ((a1 - b1) * x1) + ((a2 - b2) * x2) by A2, Th25 ;
then ( a1 - b1 = 0 & a2 - b2 = 0 ) by A1;
hence ( a1 = b1 & a2 = b2 ) ; :: thesis: verum