let T be RealLinearSpace; :: thesis:
let AV be Subset of (RLSp2RVSp T); :: thesis:
let AR be Subset of T; :: thesis:
assume A1: AV = AR ; :: thesis:

hereby :: thesis:

assume A2: AV is linearly-independent ; :: thesis:

let L be Linear_Combination of AR; :: thesis:
reconsider L1 = L as Linear_Combination of RLSp2RVSp T by Th72;
A3: Carrier L1 = Carrier L by Th73;
assume Sum L = 0. T ; :: thesis:
then A4: 0. (RLSp2RVSp T) = Sum L1 by Th76;
L1 is Linear_Combination of AV by A1, A3, RLVECT_2:def 6, VECTSP_6:def 4;
hence Carrier L = {} by A2, A3, A4, VECTSP_7:def 1; :: thesis:

end;

hence AR is linearly-independent by RLVECT_3:def 1; :: thesis:

end;

assume A5: AR is linearly-independent ; :: thesis:

let L be Linear_Combination of AV; :: thesis:
reconsider L1 = L as Linear_Combination of T by Th72;
A6: Carrier L1 = Carrier L by Th73;
reconsider L1 = L1 as Linear_Combination of AR by VECTSP_6:def 4, A1, A6, RLVECT_2:def 6;
assume Sum L = 0. (RLSp2RVSp T) ; :: thesis:
then 0. T = Sum L1 by Th76;
hence Carrier L = {} by A5, A6, RLVECT_3:def 1; :: thesis:

end;

hence AV is linearly-independent by VECTSP_7:def 1; :: thesis: