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)))

proof

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;

for a being Real
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

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;

then consider W being strict Subspace of TOP-REAL n such that
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

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;

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;
(Lin A) /\ (Lin A2) = (0). (TOP-REAL n)

proof

for v being VECTOR of (TOP-REAL n) holds
( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) )

proof

let v be VECTOR of (TOP-REAL n); :: thesis: ( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) )

hereby :: thesis: ( v in (0). (TOP-REAL n) implies 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;

assume v in (0). (TOP-REAL n) ; :: thesis: v in (Lin A) /\ (Lin A2)
then v = 0. (TOP-REAL n) by RLVECT_3:29;
hence v in (Lin A) /\ (Lin A2) by RLSUB_1:17; :: thesis: verum

end;

hence (Lin A) /\ (Lin A2) = (0). (TOP-REAL n) by RLSUB_1:31; :: thesis: verum

end;

then dim (TOP-REAL n) = (dim (Lin A)) + (dim (Lin A2)) by RLVECT_5:37, A13, RLSUB_2:def 4;
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