let n be Nat; :: thesis: for X being set holds
( X is affinely-independent Subset of (REAL-NS n) iff X is affinely-independent Subset of (TOP-REAL n) )
let X be set ; :: thesis: ( X is affinely-independent Subset of (REAL-NS n) iff X is affinely-independent Subset of (TOP-REAL n) )

hereby :: thesis: ( X is affinely-independent Subset of (TOP-REAL n) implies X is affinely-independent Subset of (REAL-NS n) )

assume X is affinely-independent Subset of (REAL-NS n) ; :: thesis: X is affinely-independent Subset of (TOP-REAL n)
then reconsider Ar = X as affinely-independent Subset of (REAL-NS n) ;
reconsider At = Ar as Subset of (TOP-REAL n) by Th4;

per cases ( Ar is empty or ex v being VECTOR of (REAL-NS n) st
( v in Ar & ((- v) + Ar) \ {(0. (REAL-NS n))} is linearly-independent ) ) by RLAFFIN1:def 4;

suppose Ar is empty ; :: thesis: X is affinely-independent Subset of (TOP-REAL n)

then At is empty ;
hence X is affinely-independent Subset of (TOP-REAL n) ; :: thesis: verum

end;

suppose ex v being VECTOR of (REAL-NS n) st
( v in Ar & ((- v) + Ar) \ {(0. (REAL-NS n))} is linearly-independent ) ; :: thesis: X is affinely-independent Subset of (TOP-REAL n)

then consider v being VECTOR of (REAL-NS n) such that
A1: ( v in Ar & ((- v) + Ar) \ {(0. (REAL-NS n))} is linearly-independent ) ;
reconsider w = v as VECTOR of (TOP-REAL n) by Th4;
A2: 0. (REAL-NS n) = 0. (TOP-REAL n) by Th6;
((- v) + Ar) \ {(0. (REAL-NS n))} = ((- w) + At) \ {(0. (TOP-REAL n))} by A2, Th9, Th39;
then ((- w) + At) \ {(0. (TOP-REAL n))} is linearly-independent by A1, Th28;
hence X is affinely-independent Subset of (TOP-REAL n) by A1, RLAFFIN1:def 4; :: thesis: verum

end;

end;

end;

assume X is affinely-independent Subset of (TOP-REAL n) ; :: thesis: X is affinely-independent Subset of (REAL-NS n)
then reconsider At = X as affinely-independent Subset of (TOP-REAL n) ;
reconsider Ar = At as Subset of (REAL-NS n) by Th4;

per cases ( At is empty or ex v being VECTOR of (TOP-REAL n) st
( v in At & ((- v) + At) \ {(0. (TOP-REAL n))} is linearly-independent ) ) by RLAFFIN1:def 4;

suppose At is empty ; :: thesis: X is affinely-independent Subset of (REAL-NS n)

then Ar is empty ;
hence X is affinely-independent Subset of (REAL-NS n) ; :: thesis: verum

end;

suppose ex v being VECTOR of (TOP-REAL n) st
( v in At & ((- v) + At) \ {(0. (TOP-REAL n))} is linearly-independent ) ; :: thesis: X is affinely-independent Subset of (REAL-NS n)

then consider v being VECTOR of (TOP-REAL n) such that
A3: ( v in At & ((- v) + At) \ {(0. (TOP-REAL n))} is linearly-independent ) ;
reconsider w = v as VECTOR of (REAL-NS n) by Th4;
A4: 0. (REAL-NS n) = 0. (TOP-REAL n) by Th6;
((- w) + Ar) \ {(0. (REAL-NS n))} = ((- v) + At) \ {(0. (TOP-REAL n))} by A4, Th9, Th39;
then ((- w) + Ar) \ {(0. (REAL-NS n))} is linearly-independent by A3, Th28;
hence X is affinely-independent Subset of (REAL-NS n) by A3, RLAFFIN1:def 4; :: thesis: verum

end;

end;