let GF be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for V being strict VectSp of GF
for A being Subset of V st A = the carrier of V holds
Lin A = V
let V be strict VectSp of GF; :: thesis: for A being Subset of V st A = the carrier of V holds
Lin A = V
let A be Subset of V; :: 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, Th11; :: thesis: verum