let V be RealUnitarySpace; :: thesis: for A being non empty Affine Subset of V st 0. V in A holds

A = the carrier of (Lin A)

let A be non empty Affine Subset of V; :: thesis: ( 0. V in A implies A = the carrier of (Lin A) )

assume 0. V in A ; :: thesis: A = the carrier of (Lin A)

then A1: A is Subspace-like by Th26;

for x being object st x in the carrier of (Lin A) holds

x in A

for x being object st x in A holds

x in the carrier of (Lin A) by RUSUB_3:2, STRUCT_0:def 5;

then A c= the carrier of (Lin A) ;

hence A = the carrier of (Lin A) by A3; :: thesis: verum

A = the carrier of (Lin A)

let A be non empty Affine Subset of V; :: thesis: ( 0. V in A implies A = the carrier of (Lin A) )

assume 0. V in A ; :: thesis: A = the carrier of (Lin A)

then A1: A is Subspace-like by Th26;

for x being object st x in the carrier of (Lin A) holds

x in A

proof

then A3:
the carrier of (Lin A) c= A
;
let x be object ; :: 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 ;

then A2: ex l being Linear_Combination of A st x = Sum l by RUSUB_3:1;

( ( 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 A1;

then A is linearly-closed by RLSUB_1:def 1;

hence x in A by A2, RLVECT_2:29; :: thesis: verum

end;assume x in the carrier of (Lin A) ; :: thesis: x in A

then x in Lin A ;

then A2: ex l being Linear_Combination of A st x = Sum l by RUSUB_3:1;

( ( 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 A1;

then A is linearly-closed by RLSUB_1:def 1;

hence x in A by A2, RLVECT_2:29; :: thesis: verum

for x being object st x in A holds

x in the carrier of (Lin A) by RUSUB_3:2, STRUCT_0:def 5;

then A c= the carrier of (Lin A) ;

hence A = the carrier of (Lin A) by A3; :: thesis: verum