let n be Element of NAT ; :: thesis: for A being Subset of (REAL n)
for x being Element of REAL n st A is being_plane & x in A & ex a being Real st
( a <> 1 & a * x in A ) holds
0* n in A
let A be Subset of (REAL n); :: thesis: for x being Element of REAL n st A is being_plane & x in A & ex a being Real st
( a <> 1 & a * x in A ) holds
0* n in A
let x be Element of REAL n; :: thesis: ( A is being_plane & x in A & ex a being Real st
( a <> 1 & a * x in A ) implies 0* n in A )
assume A1: ( A is being_plane & x in A & ex a being Real st
( a <> 1 & a * x in A ) ) ; :: thesis: 0* n in A
then consider x1, x2, x3 being Element of REAL n such that
A2: ( x2 - x1,x3 - x1 are_lindependent2 & A = plane x1,x2,x3 ) by Def10;
consider a being Real such that
A3: ( a <> 1 & a * x in A ) by A1;
A4: Line x,(a * x) c= A by A1, A2, A3, Th90;
A5: 1 - a <> 0 by A3;
A6: (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 A5, XCMPLX_1:60
.= 0 ;
0* n = 0 * x by EUCLID_4:3
.= ((1 - (1 / (1 - a))) * x) + (((1 / (1 - a)) * a) * x) by A6, 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 A by A4; :: thesis: verum