let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
let W be Subspace of V; :: thesis: for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
let A be Subset of V; :: thesis: ( A c= the carrier of W implies Lin A is Subspace of W )
assume A1: A c= the carrier of W ; :: thesis: Lin A is Subspace of W
now :: thesis: for w being object st w in the carrier of (Lin A) holds
w in the carrier of W
let w be object ; :: thesis: ( w in the carrier of (Lin A) implies w in the carrier of W )
assume w in the carrier of (Lin A) ; :: thesis: w in the carrier of W
then w in Lin A by STRUCT_0:def 5;
then consider L being Linear_Combination of A such that
A2: w = Sum L by Th1;
Carrier L c= A by RLVECT_2:def 6;
then ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum L = Sum K ) by A1, Th20, XBOOLE_1:1;
hence w in the carrier of W by A2; :: thesis: verum
end;
then the carrier of (Lin A) c= the carrier of W ;
hence Lin A is Subspace of W by RUSUB_1:22; :: thesis: verum