let V be finite-dimensional RealUnitarySpace; :: thesis: for A being Subset of V st A is linearly-independent holds

card A = dim (Lin A)

let A be Subset of V; :: thesis: ( A is linearly-independent implies card A = dim (Lin A) )

assume A1: A is linearly-independent ; :: thesis: card A = dim (Lin A)

set W = Lin A;

for x being object st x in A holds

x in the carrier of (Lin A) by STRUCT_0:def 5, RUSUB_3:2;

then reconsider B = A as linearly-independent Subset of (Lin A) by A1, RUSUB_3:23, TARSKI:def 3;

Lin A = Lin B by RUSUB_3:28;

then reconsider B = B as Basis of Lin A by RUSUB_3:def 2;

card B = dim (Lin A) by Def2;

hence card A = dim (Lin A) ; :: thesis: verum

card A = dim (Lin A)

let A be Subset of V; :: thesis: ( A is linearly-independent implies card A = dim (Lin A) )

assume A1: A is linearly-independent ; :: thesis: card A = dim (Lin A)

set W = Lin A;

for x being object st x in A holds

x in the carrier of (Lin A) by STRUCT_0:def 5, RUSUB_3:2;

then reconsider B = A as linearly-independent Subset of (Lin A) by A1, RUSUB_3:23, TARSKI:def 3;

Lin A = Lin B by RUSUB_3:28;

then reconsider B = B as Basis of Lin A by RUSUB_3:def 2;

card B = dim (Lin A) by Def2;

hence card A = dim (Lin A) ; :: thesis: verum