let n be Nat; :: thesis: for p being Point of () st p <> 0. () holds
ex A being linearly-independent Subset of () st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. ())) )

let p be Point of (); :: thesis: ( p <> 0. () implies ex A being linearly-independent Subset of () st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. ())) ) )

assume A1: p <> 0. () ; :: thesis: ex A being linearly-independent Subset of () st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. ())) )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
A2: 0. () = - (0. (TOP-REAL n1)) by JGRAPH_5:10
.= - (0. ()) ;
set V1 = Plane (p,(0. ()));
|(p,(0. ()))| = 0 by EUCLID_2:32;
then |(p,((0. ()) - (0. ())))| = 0 by RLVECT_1:5;
then A3: 0. () in Plane (p,(0. ())) ;
A4: for v, u being VECTOR of () st v in Plane (p,(0. ())) & u in Plane (p,(0. ())) holds
v + u in Plane (p,(0. ()))
proof
let v, u be VECTOR of (); :: thesis: ( v in Plane (p,(0. ())) & u in Plane (p,(0. ())) implies v + u in Plane (p,(0. ())) )
assume v in Plane (p,(0. ())) ; :: thesis: ( not u in Plane (p,(0. ())) or v + u in Plane (p,(0. ())) )
then consider v1 being Point of () such that
A5: ( v = v1 & |(p,(v1 - (0. ())))| = 0 ) ;
assume u in Plane (p,(0. ())) ; :: thesis: v + u in Plane (p,(0. ()))
then consider u1 being Point of () such that
A6: ( u = u1 & |(p,(u1 - (0. ())))| = 0 ) ;
|(p,((v1 + u1) - (0. ())))| = |(p,(v1 + (u1 - (0. ()))))| by RLVECT_1:def 3
.= |(p,v1)| + |(p,(u1 - (0. ())))| by EUCLID_2:26
.= 0 by ;
hence v + u in Plane (p,(0. ())) by A5, A6; :: thesis: verum
end;
for a being Real
for v being VECTOR of () st v in Plane (p,(0. ())) holds
a * v in Plane (p,(0. ()))
proof
let a be Real; :: thesis: for v being VECTOR of () st v in Plane (p,(0. ())) holds
a * v in Plane (p,(0. ()))

let v be VECTOR of (); :: thesis: ( v in Plane (p,(0. ())) implies a * v in Plane (p,(0. ())) )
assume v in Plane (p,(0. ())) ; :: thesis: a * v in Plane (p,(0. ()))
then consider v1 being Point of () such that
A7: ( v = v1 & |(p,(v1 - (0. ())))| = 0 ) ;
|(p,(a * (v1 - (0. ()))))| = a * 0 by ;
then |(p,((a * v1) - (a * (0. ()))))| = 0 by RLVECT_1:34;
then |(p,((a * v1) - (0. ())))| = 0 by RLVECT_1:10;
hence a * v in Plane (p,(0. ())) by A7; :: thesis: verum
end;
then consider W being strict Subspace of TOP-REAL n such that
A8: Plane (p,(0. ())) = the carrier of W by ;
set A1 = the Basis of W;
A10: [#] (Lin the Basis of W) = Plane (p,(0. ())) by ;
reconsider A = the Basis of W as linearly-independent Subset of () by ;
take A ; :: thesis: ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. ())) )
reconsider A2 = {p} as linearly-independent Subset of () by ;
A11: dim (Lin A2) = card A2 by RLVECT_5:29
.= 1 by CARD_1:30 ;
for v being VECTOR of () ex v1, v2 being VECTOR of () st
( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )
proof
let v be VECTOR of (); :: thesis: ex v1, v2 being VECTOR of () 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 () ;
take v1 ; :: thesis: ex v2 being VECTOR of () 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 ;
|(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
.= 0 ;
then |(p,(v1 - (0. ())))| = 0 by ;
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 (), the ZeroF of (), the U5 of (), the Mult of () #) = (Lin A) + (Lin A2) by RLSUB_2:44;
(Lin A) /\ (Lin A2) = (0). ()
proof
for v being VECTOR of () holds
( v in (Lin A) /\ (Lin A2) iff v in (0). () )
proof
let v be VECTOR of (); :: thesis: ( v in (Lin A) /\ (Lin A2) iff v in (0). () )
hereby :: thesis: ( v in (0). () implies v in (Lin A) /\ (Lin A2) )
assume v in (Lin A) /\ (Lin A2) ; :: thesis: v in (0). ()
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. ())) by ;
then consider y being Point of () such that
A16: ( y = v & |(p,(y - (0. ())))| = 0 ) ;
|(p,v)| = 0 by ;
then A17: a * |(p,p)| = 0 by ;
|(p,p)| > 0 by ;
then a = 0 by A17;
then v = 0. () by ;
hence v in (0). () by RLVECT_3:29; :: thesis: verum
end;
assume v in (0). () ; :: thesis: v in (Lin A) /\ (Lin A2)
then v = 0. () by RLVECT_3:29;
hence v in (Lin A) /\ (Lin A2) by RLSUB_1:17; :: thesis: verum
end;
hence (Lin A) /\ (Lin A2) = (0). () by RLSUB_1:31; :: thesis: verum
end;
then dim () = (dim (Lin A)) + (dim (Lin A2)) by ;
then n = (dim (Lin A)) + 1 by ;
hence card A = n - 1 by RLVECT_5:29; :: thesis: [#] (Lin A) = Plane (p,(0. ()))
thus [#] (Lin A) = Plane (p,(0. ())) by ; :: thesis: verum