let n be Nat; :: thesis: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds

ex A being linearly-independent Subset of (TOP-REAL n) st

( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )

let p be Point of (TOP-REAL n); :: thesis: ( p <> 0. (TOP-REAL n) implies ex A being linearly-independent Subset of (TOP-REAL n) st

( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) ) )

assume A1: p <> 0. (TOP-REAL n) ; :: thesis: ex A being linearly-independent Subset of (TOP-REAL n) st

( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A2: 0. (TOP-REAL n) = - (0. (TOP-REAL n1)) by JGRAPH_5:10

.= - (0. (TOP-REAL n)) ;

set V1 = Plane (p,(0. (TOP-REAL n)));

|(p,(0. (TOP-REAL n)))| = 0 by EUCLID_2:32;

then |(p,((0. (TOP-REAL n)) - (0. (TOP-REAL n))))| = 0 by RLVECT_1:5;

then A3: 0. (TOP-REAL n) in Plane (p,(0. (TOP-REAL n))) ;

A4: for v, u being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) & u in Plane (p,(0. (TOP-REAL n))) holds

v + u in Plane (p,(0. (TOP-REAL n)))

for v being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) holds

a * v in Plane (p,(0. (TOP-REAL n)))

A8: Plane (p,(0. (TOP-REAL n))) = the carrier of W by A3, RLSUB_1:35, A4, RLSUB_1:def 1;

set A1 = the Basis of W;

A10: [#] (Lin the Basis of W) = Plane (p,(0. (TOP-REAL n))) by A8, RLVECT_3:def 3;

reconsider A = the Basis of W as linearly-independent Subset of (TOP-REAL n) by RLVECT_3:def 3, RLVECT_5:14;

take A ; :: thesis: ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )

reconsider A2 = {p} as linearly-independent Subset of (TOP-REAL n) by A1, RLVECT_3:8;

A11: dim (Lin A2) = card A2 by RLVECT_5:29

.= 1 by CARD_1:30 ;

for v being VECTOR of (TOP-REAL n) ex v1, v2 being VECTOR of (TOP-REAL n) st

( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )

(Lin A) /\ (Lin A2) = (0). (TOP-REAL n)

then n = (dim (Lin A)) + 1 by A11, RLAFFIN3:4;

hence card A = n - 1 by RLVECT_5:29; :: thesis: [#] (Lin A) = Plane (p,(0. (TOP-REAL n)))

thus [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) by A10, RLVECT_5:20; :: thesis: verum

ex A being linearly-independent Subset of (TOP-REAL n) st

( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )

let p be Point of (TOP-REAL n); :: thesis: ( p <> 0. (TOP-REAL n) implies ex A being linearly-independent Subset of (TOP-REAL n) st

( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) ) )

assume A1: p <> 0. (TOP-REAL n) ; :: thesis: ex A being linearly-independent Subset of (TOP-REAL n) st

( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A2: 0. (TOP-REAL n) = - (0. (TOP-REAL n1)) by JGRAPH_5:10

.= - (0. (TOP-REAL n)) ;

set V1 = Plane (p,(0. (TOP-REAL n)));

|(p,(0. (TOP-REAL n)))| = 0 by EUCLID_2:32;

then |(p,((0. (TOP-REAL n)) - (0. (TOP-REAL n))))| = 0 by RLVECT_1:5;

then A3: 0. (TOP-REAL n) in Plane (p,(0. (TOP-REAL n))) ;

A4: for v, u being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) & u in Plane (p,(0. (TOP-REAL n))) holds

v + u in Plane (p,(0. (TOP-REAL n)))

proof

for a being Real
let v, u be VECTOR of (TOP-REAL n); :: thesis: ( v in Plane (p,(0. (TOP-REAL n))) & u in Plane (p,(0. (TOP-REAL n))) implies v + u in Plane (p,(0. (TOP-REAL n))) )

assume v in Plane (p,(0. (TOP-REAL n))) ; :: thesis: ( not u in Plane (p,(0. (TOP-REAL n))) or v + u in Plane (p,(0. (TOP-REAL n))) )

then consider v1 being Point of (TOP-REAL n) such that

A5: ( v = v1 & |(p,(v1 - (0. (TOP-REAL n))))| = 0 ) ;

assume u in Plane (p,(0. (TOP-REAL n))) ; :: thesis: v + u in Plane (p,(0. (TOP-REAL n)))

then consider u1 being Point of (TOP-REAL n) such that

A6: ( u = u1 & |(p,(u1 - (0. (TOP-REAL n))))| = 0 ) ;

|(p,((v1 + u1) - (0. (TOP-REAL n))))| = |(p,(v1 + (u1 - (0. (TOP-REAL n)))))| by RLVECT_1:def 3

.= |(p,v1)| + |(p,(u1 - (0. (TOP-REAL n))))| by EUCLID_2:26

.= 0 by A5, A2, A6, RLVECT_1:4 ;

hence v + u in Plane (p,(0. (TOP-REAL n))) by A5, A6; :: thesis: verum

end;assume v in Plane (p,(0. (TOP-REAL n))) ; :: thesis: ( not u in Plane (p,(0. (TOP-REAL n))) or v + u in Plane (p,(0. (TOP-REAL n))) )

then consider v1 being Point of (TOP-REAL n) such that

A5: ( v = v1 & |(p,(v1 - (0. (TOP-REAL n))))| = 0 ) ;

assume u in Plane (p,(0. (TOP-REAL n))) ; :: thesis: v + u in Plane (p,(0. (TOP-REAL n)))

then consider u1 being Point of (TOP-REAL n) such that

A6: ( u = u1 & |(p,(u1 - (0. (TOP-REAL n))))| = 0 ) ;

|(p,((v1 + u1) - (0. (TOP-REAL n))))| = |(p,(v1 + (u1 - (0. (TOP-REAL n)))))| by RLVECT_1:def 3

.= |(p,v1)| + |(p,(u1 - (0. (TOP-REAL n))))| by EUCLID_2:26

.= 0 by A5, A2, A6, RLVECT_1:4 ;

hence v + u in Plane (p,(0. (TOP-REAL n))) by A5, A6; :: thesis: verum

for v being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) holds

a * v in Plane (p,(0. (TOP-REAL n)))

proof

then consider W being strict Subspace of TOP-REAL n such that
let a be Real; :: thesis: for v being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) holds

a * v in Plane (p,(0. (TOP-REAL n)))

let v be VECTOR of (TOP-REAL n); :: thesis: ( v in Plane (p,(0. (TOP-REAL n))) implies a * v in Plane (p,(0. (TOP-REAL n))) )

assume v in Plane (p,(0. (TOP-REAL n))) ; :: thesis: a * v in Plane (p,(0. (TOP-REAL n)))

then consider v1 being Point of (TOP-REAL n) such that

A7: ( v = v1 & |(p,(v1 - (0. (TOP-REAL n))))| = 0 ) ;

|(p,(a * (v1 - (0. (TOP-REAL n)))))| = a * 0 by A7, EUCLID_2:20;

then |(p,((a * v1) - (a * (0. (TOP-REAL n)))))| = 0 by RLVECT_1:34;

then |(p,((a * v1) - (0. (TOP-REAL n))))| = 0 by RLVECT_1:10;

hence a * v in Plane (p,(0. (TOP-REAL n))) by A7; :: thesis: verum

end;a * v in Plane (p,(0. (TOP-REAL n)))

let v be VECTOR of (TOP-REAL n); :: thesis: ( v in Plane (p,(0. (TOP-REAL n))) implies a * v in Plane (p,(0. (TOP-REAL n))) )

assume v in Plane (p,(0. (TOP-REAL n))) ; :: thesis: a * v in Plane (p,(0. (TOP-REAL n)))

then consider v1 being Point of (TOP-REAL n) such that

A7: ( v = v1 & |(p,(v1 - (0. (TOP-REAL n))))| = 0 ) ;

|(p,(a * (v1 - (0. (TOP-REAL n)))))| = a * 0 by A7, EUCLID_2:20;

then |(p,((a * v1) - (a * (0. (TOP-REAL n)))))| = 0 by RLVECT_1:34;

then |(p,((a * v1) - (0. (TOP-REAL n))))| = 0 by RLVECT_1:10;

hence a * v in Plane (p,(0. (TOP-REAL n))) by A7; :: thesis: verum

A8: Plane (p,(0. (TOP-REAL n))) = the carrier of W by A3, RLSUB_1:35, A4, RLSUB_1:def 1;

set A1 = the Basis of W;

A10: [#] (Lin the Basis of W) = Plane (p,(0. (TOP-REAL n))) by A8, RLVECT_3:def 3;

reconsider A = the Basis of W as linearly-independent Subset of (TOP-REAL n) by RLVECT_3:def 3, RLVECT_5:14;

take A ; :: thesis: ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )

reconsider A2 = {p} as linearly-independent Subset of (TOP-REAL n) by A1, RLVECT_3:8;

A11: dim (Lin A2) = card A2 by RLVECT_5:29

.= 1 by CARD_1:30 ;

for v being VECTOR of (TOP-REAL n) ex v1, v2 being VECTOR of (TOP-REAL n) st

( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )

proof

then A13:
RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) = (Lin A) + (Lin A2)
by RLSUB_2:44;
let v be VECTOR of (TOP-REAL n); :: thesis: ex v1, v2 being VECTOR of (TOP-REAL n) st

( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )

set a = |(p,v)| / |(p,p)|;

set v2 = (|(p,v)| / |(p,p)|) * p;

set v1 = v - ((|(p,v)| / |(p,p)|) * p);

reconsider v1 = v - ((|(p,v)| / |(p,p)|) * p), v2 = (|(p,v)| / |(p,p)|) * p as VECTOR of (TOP-REAL n) ;

take v1 ; :: thesis: ex v2 being VECTOR of (TOP-REAL n) st

( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )

take v2 ; :: thesis: ( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )

A12: |(p,p)| > 0 by A1, EUCLID_2:43;

|(p,v1)| = |(p,v)| - |(p,v2)| by EUCLID_2:27

.= |(p,v)| - ((|(p,v)| / |(p,p)|) * |(p,p)|) by EUCLID_2:20

.= |(p,v)| - |(p,v)| by A12, XCMPLX_1:87

.= 0 ;

then |(p,(v1 - (0. (TOP-REAL n))))| = 0 by A2, RLVECT_1:4;

then v1 in Lin the Basis of W by A10;

hence v1 in Lin A by RLVECT_5:20; :: thesis: ( v2 in Lin A2 & v = v1 + v2 )

thus v2 in Lin A2 by RLVECT_4:8; :: thesis: v = v1 + v2

thus v = v1 + v2 by RLVECT_4:1; :: thesis: verum

end;( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )

set a = |(p,v)| / |(p,p)|;

set v2 = (|(p,v)| / |(p,p)|) * p;

set v1 = v - ((|(p,v)| / |(p,p)|) * p);

reconsider v1 = v - ((|(p,v)| / |(p,p)|) * p), v2 = (|(p,v)| / |(p,p)|) * p as VECTOR of (TOP-REAL n) ;

take v1 ; :: thesis: ex v2 being VECTOR of (TOP-REAL n) st

( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )

take v2 ; :: thesis: ( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )

A12: |(p,p)| > 0 by A1, EUCLID_2:43;

|(p,v1)| = |(p,v)| - |(p,v2)| by EUCLID_2:27

.= |(p,v)| - ((|(p,v)| / |(p,p)|) * |(p,p)|) by EUCLID_2:20

.= |(p,v)| - |(p,v)| by A12, XCMPLX_1:87

.= 0 ;

then |(p,(v1 - (0. (TOP-REAL n))))| = 0 by A2, RLVECT_1:4;

then v1 in Lin the Basis of W by A10;

hence v1 in Lin A by RLVECT_5:20; :: thesis: ( v2 in Lin A2 & v = v1 + v2 )

thus v2 in Lin A2 by RLVECT_4:8; :: thesis: v = v1 + v2

thus v = v1 + v2 by RLVECT_4:1; :: thesis: verum

(Lin A) /\ (Lin A2) = (0). (TOP-REAL n)

proof

then
dim (TOP-REAL n) = (dim (Lin A)) + (dim (Lin A2))
by RLVECT_5:37, A13, RLSUB_2:def 4;
for v being VECTOR of (TOP-REAL n) holds

( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) )

end;( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) )

proof

hence
(Lin A) /\ (Lin A2) = (0). (TOP-REAL n)
by RLSUB_1:31; :: thesis: verum
let v be VECTOR of (TOP-REAL n); :: thesis: ( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) )

then v = 0. (TOP-REAL n) by RLVECT_3:29;

hence v in (Lin A) /\ (Lin A2) by RLSUB_1:17; :: thesis: verum

end;hereby :: thesis: ( v in (0). (TOP-REAL n) implies v in (Lin A) /\ (Lin A2) )

assume
v in (0). (TOP-REAL n)
; :: thesis: v in (Lin A) /\ (Lin A2)assume
v in (Lin A) /\ (Lin A2)
; :: thesis: v in (0). (TOP-REAL n)

then A14: ( v in Lin A & v in Lin A2 ) by RLSUB_2:3;

then consider a being Real such that

A15: v = a * p by RLVECT_4:8;

v in Plane (p,(0. (TOP-REAL n))) by A10, A14, RLVECT_5:20;

then consider y being Point of (TOP-REAL n) such that

A16: ( y = v & |(p,(y - (0. (TOP-REAL n))))| = 0 ) ;

|(p,v)| = 0 by A2, A16, RLVECT_1:4;

then A17: a * |(p,p)| = 0 by A15, EUCLID_2:20;

|(p,p)| > 0 by A1, EUCLID_2:43;

then a = 0 by A17;

then v = 0. (TOP-REAL n) by A15, RLVECT_1:10;

hence v in (0). (TOP-REAL n) by RLVECT_3:29; :: thesis: verum

end;then A14: ( v in Lin A & v in Lin A2 ) by RLSUB_2:3;

then consider a being Real such that

A15: v = a * p by RLVECT_4:8;

v in Plane (p,(0. (TOP-REAL n))) by A10, A14, RLVECT_5:20;

then consider y being Point of (TOP-REAL n) such that

A16: ( y = v & |(p,(y - (0. (TOP-REAL n))))| = 0 ) ;

|(p,v)| = 0 by A2, A16, RLVECT_1:4;

then A17: a * |(p,p)| = 0 by A15, EUCLID_2:20;

|(p,p)| > 0 by A1, EUCLID_2:43;

then a = 0 by A17;

then v = 0. (TOP-REAL n) by A15, RLVECT_1:10;

hence v in (0). (TOP-REAL n) by RLVECT_3:29; :: thesis: verum

then v = 0. (TOP-REAL n) by RLVECT_3:29;

hence v in (Lin A) /\ (Lin A2) by RLSUB_1:17; :: thesis: verum

then n = (dim (Lin A)) + 1 by A11, RLAFFIN3:4;

hence card A = n - 1 by RLVECT_5:29; :: thesis: [#] (Lin A) = Plane (p,(0. (TOP-REAL n)))

thus [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) by A10, RLVECT_5:20; :: thesis: verum