let a be Real; :: thesis: for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st x in L & a <> 1 & a * x in L holds
0* n in L
let n be Nat; :: thesis: for x being Element of REAL n
for L being Element of line_of_REAL n st x in L & a <> 1 & a * x in L holds
0* n in L
let x be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st x in L & a <> 1 & a * x in L holds
0* n in L
let L be Element of line_of_REAL n; :: thesis: ( x in L & a <> 1 & a * x in L implies 0* n in L )
assume that
A1: x in L and
A2: a <> 1 and
A3: a * x in L ; :: thesis: 0* n in L
A4: 1 - a <> 0 by A2;
A5: (1 - (1 / (1 - a))) + ((1 / (1 - a)) * a) = (1 - (1 / (1 - a))) + (a / (1 - a)) by XCMPLX_1:99
.= 1 + ((- (1 / (1 - a))) + (a / (1 - a)))
.= 1 + (((- 1) / (1 - a)) + (a / (1 - a))) by XCMPLX_1:187
.= 1 + (((- 1) + a) / (1 - a)) by XCMPLX_1:62
.= 1 + ((- ((- a) + 1)) / (1 - a))
.= 1 + (- ((1 - a) / (1 - a))) by XCMPLX_1:187
.= 1 - ((1 - a) / (1 - a))
.= 1 - 1 by A4, XCMPLX_1:60
.= 0 ;
0* n = 0 * x by EUCLID_4:3
.= ((1 - (1 / (1 - a))) * x) + (((1 / (1 - a)) * a) * x) by A5, EUCLID_4:7
.= ((1 - (1 / (1 - a))) * x) + ((1 / (1 - a)) * (a * x)) by EUCLID_4:4 ;
then A6: 0* n in Line (x,(a * x)) ;
Line (x,(a * x)) c= L by A1, A3, Th48;
hence 0* n in L by A6; :: thesis: verum