let a be Real; :: thesis: for n being Element of 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 Element of 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 A1: ( x in L & a <> 1 & a * x in L ) ; :: thesis: 0* n in L
then A2: Line x,(a * x) c= L by Th53;
A3: 1 - a <> 0 by A1;
A4: (1 - (1 / (1 - a))) + ((1 / (1 - a)) * a) = (1 - (1 / (1 - a))) + (a / (1 - a)) by XCMPLX_1:100
.= 1 + ((- (1 / (1 - a))) + (a / (1 - a)))
.= 1 + (((- 1) / (1 - a)) + (a / (1 - a))) by XCMPLX_1:188
.= 1 + (((- 1) + a) / (1 - a)) by XCMPLX_1:63
.= 1 + ((- ((- a) + 1)) / (1 - a))
.= 1 + (- ((1 - a) / (1 - a))) by XCMPLX_1:188
.= 1 - ((1 - a) / (1 - a))
.= 1 - 1 by A3, XCMPLX_1:60
.= 0 ;
0* n = 0 * x by EUCLID_4:3
.= ((1 - (1 / (1 - a))) * x) + (((1 / (1 - a)) * a) * x) by A4, EUCLID_4:7
.= ((1 - (1 / (1 - a))) * x) + ((1 / (1 - a)) * (a * x)) by EUCLID_4:4 ;
then 0* n in Line x,(a * x) ;
hence 0* n in L by A2; :: thesis: verum