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 non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let A, B be Subset of V; :: thesis: ( Lin A = V & A c= B implies Lin B = V )
assume that
A1: Lin A = V and
A2: A c= B ; :: thesis: Lin B = V
V is Subspace of Lin B by A1, A2, Th13;
hence Lin B = V by A1, VECTSP_4:25; :: thesis: verum