let V be RealLinearSpace; :: thesis: for A being Subset of V

for W being strict Subspace of V st A = the carrier of W holds

Lin A = W

let A be Subset of V; :: thesis: for W being strict Subspace of V st A = the carrier of W holds

Lin A = W

let W be strict Subspace of V; :: thesis: ( A = the carrier of W implies Lin A = W )

assume A1: A = the carrier of W ; :: thesis: Lin A = W

for W being strict Subspace of V st A = the carrier of W holds

Lin A = W

let A be Subset of V; :: thesis: for W being strict Subspace of V st A = the carrier of W holds

Lin A = W

let W be strict Subspace 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 ) )

hence
Lin A = W
by RLSUB_1:31; :: thesis: verum( ( 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 )

hence ( v in W implies v in Lin A ) by A1, Th15; :: thesis: verum

end;thus ( v in Lin A implies v in W ) :: thesis: ( v in W implies v in Lin A )

proof

( v in W iff v in the carrier of W )
by STRUCT_0:def 5;
assume
v in Lin A
; :: thesis: v in W

then A2: ex l being Linear_Combination of A st v = Sum l by Th14;

A is linearly-closed by A1, RLSUB_1:34;

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;then A2: ex l being Linear_Combination of A st v = Sum l by Th14;

A is linearly-closed by A1, RLSUB_1:34;

then v in the carrier of W by A1, A2, RLVECT_2:29;

hence v in W by STRUCT_0:def 5; :: thesis: verum

hence ( v in W implies v in Lin A ) by A1, Th15; :: thesis: verum