let V be RealUnitarySpace; :: thesis: for W being strict Subspace of V
for A being Subset of V st A = the carrier of W holds
Lin A = W
let W be strict Subspace of V; :: thesis: for A being Subset of V st A = the carrier of W holds
Lin A = W
let A be Subset of V; :: thesis: ( A = the carrier of W implies Lin A = W )
assume A1: A = the carrier of W ; :: thesis: Lin A = W
now :: thesis: for v being VECTOR of V holds
( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) )
let v be VECTOR of V; :: thesis: ( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) )
thus ( v in Lin A implies v in W ) :: thesis: ( v in W implies v in Lin A )
proof
assume v in Lin A ; :: thesis: v in W
then A2: ex l being Linear_Combination of A st v = Sum l by Th1;
A is linearly-closed by A1, RUSUB_1:28;
then v in the carrier of W by A1, A2, RLVECT_2:29;
hence v in W by STRUCT_0:def 5; :: thesis: verum
end;
( v in W iff v in the carrier of W ) by STRUCT_0:def 5;
hence ( v in W implies v in Lin A ) by A1, Th2; :: thesis: verum
end;
hence Lin A = W by RUSUB_1:25; :: thesis: verum