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