let V be RealLinearSpace; :: thesis: for A being non empty Affine Subset of V st 0. V in A holds
( A is Subspace-like & A = the carrier of (Lin A) )
let A be non empty Affine Subset of V; :: thesis: ( 0. V in A implies ( A is Subspace-like & A = the carrier of (Lin A) ) )
assume A1: 0. V in A ; :: thesis: ( A is Subspace-like & A = the carrier of (Lin A) )
A2: for x, y being Element of V
for a being Real st x in A & y in A holds
( x + y in A & a * x in A )

proof

let x, y be Element of V; :: thesis: for a being Real st x in A & y in A holds
( x + y in A & a * x in A )
let a be Real; :: thesis: ( x in A & y in A implies ( x + y in A & a * x in A ) )
assume that
A3: x in A and
A4: y in A ; :: thesis: ( x + y in A & a * x in A )
reconsider x = x, y = y as VECTOR of V ;
A5: 2 * (((1 - (1 / 2)) * x) + ((1 / 2) * y)) = (2 * ((1 - (1 / 2)) * x)) + (2 * ((1 / 2) * y)) by RLVECT_1:def 8
.= ((2 * (1 - (1 / 2))) * x) + (2 * ((1 / 2) * y)) by RLVECT_1:def 10
.= ((2 - 1) * x) + ((2 * (1 / 2)) * y) by RLVECT_1:def 10
.= x + (1 * y) by RLVECT_1:def 11
.= x + y by RLVECT_1:def 11 ;
((1 - (1 / 2)) * x) + ((1 / 2) * y) in A by A3, A4, Def5;
hence ( x + y in A & a * x in A ) by A1, A3, A5, Th25; :: thesis: verum

end;

hence A is Subspace-like by A1, Def8; :: thesis: A = the carrier of (Lin A)
for x being set st x in the carrier of (Lin A) holds
x in A

proof

let x be set ; :: thesis: ( x in the carrier of (Lin A) implies x in A )
assume x in the carrier of (Lin A) ; :: thesis: x in A
then x in Lin A by STRUCT_0:def 5;
then A6: ex l being Linear_Combination of A st x = Sum l by RLVECT_3:17;
( ( for v, u being VECTOR of V st v in A & u in A holds
v + u in A ) & ( for a being Real
for v being VECTOR of V st v in A holds
a * v in A ) ) by A2;
then A is linearly-closed by RLSUB_1:def 1;
hence x in A by A6, RLVECT_2:47; :: thesis: verum

end;

then A7: the carrier of (Lin A) c= A by TARSKI:def 3;
for x being set st x in A holds
x in the carrier of (Lin A)

proof

let x be set ; :: thesis: ( x in A implies x in the carrier of (Lin A) )
assume x in A ; :: thesis: x in the carrier of (Lin A)
then x in Lin A by RLVECT_3:18;
hence x in the carrier of (Lin A) by STRUCT_0:def 5; :: thesis: verum

end;

then A c= the carrier of (Lin A) by TARSKI:def 3;
hence A = the carrier of (Lin A) by A7, XBOOLE_0:def 10; :: thesis: verum