let V be RealLinearSpace; :: 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

hence Lin A is Subspace of W by RLSUB_1:28; :: thesis: verum

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

then
the carrier of (Lin A) c= the carrier of W
;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 RLVECT_3:14;

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, Th12, XBOOLE_1:1;

hence w in the carrier of W by A2; :: thesis: verum

end;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 RLVECT_3:14;

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, Th12, XBOOLE_1:1;

hence w in the carrier of W by A2; :: thesis: verum

hence Lin A is Subspace of W by RLSUB_1:28; :: thesis: verum