let GF be Field; :: thesis: for V being strict VectSp of strict
for A being Subset of st A = the carrier of V holds
Lin A = V
let V be strict VectSp of strict ; :: thesis: for A being Subset of st A = the carrier of V holds
Lin A = V
let A be Subset of ; :: thesis: ( A = the carrier of V implies Lin A = V )
assume A1: A = the carrier of V ; :: thesis: Lin A = V
(Omega). V = V ;
hence Lin A = V by A1, Th16; :: thesis: verum