ex B being Subset of (Lin A) st B is base

proof

hence
Lin A is free
; :: thesis: verum
for x being object st x in A holds

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

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

take B ; :: thesis: B is base

Lin B = ModuleStr(# the carrier of (Lin A), the addF of (Lin A), the ZeroF of (Lin A), the lmult of (Lin A) #) by Th20;

hence B is base ; :: thesis: verum

end;x in the carrier of (Lin A) by STRUCT_0:def 5, ZMODUL02:65;

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

take B ; :: thesis: B is base

Lin B = ModuleStr(# the carrier of (Lin A), the addF of (Lin A), the ZeroF of (Lin A), the lmult of (Lin A) #) by Th20;

hence B is base ; :: thesis: verum