let n be Nat; :: thesis:
let X be set ; :: thesis:

hereby :: thesis:

assume X is affinely-independent Subset of (REAL-NS n) ; :: thesis:
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 by RLAFFIN1:def 4;

suppose Ar is empty ; :: thesis:

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

end;

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

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:

end;

end;

end;

assume X is affinely-independent Subset of (TOP-REAL n) ; :: thesis:
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 by RLAFFIN1:def 4;

suppose At is empty ; :: thesis:

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

end;

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

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:

end;

end;