let x be set ; :: thesis: for V being RealLinearSpace

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

let V be RealLinearSpace; :: thesis: for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

let Affv be finite affinely-independent Subset of V; :: thesis: for EV being Enumeration of Affv

for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

let EV be Enumeration of Affv; :: thesis: for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

let B be Subset of V; :: thesis: ( B c= Affv & x in Affin Affv implies ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds

(x |-- EV) . y = 0 ) )

assume A1: B c= Affv ; :: thesis: ( not x in Affin Affv or ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds

(x |-- EV) . y = 0 ) )

set xA = x |-- Affv;

set xB = x |-- B;

set cA = card Affv;

set E = EV;

assume A2: x in Affin Affv ; :: thesis: ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds

(x |-- EV) . y = 0 )

set xE = x |-- EV;

A3: len (x |-- EV) = card Affv by Th16;

A4: rng EV = Affv by Def1;

then len EV = card Affv by FINSEQ_4:62;

then A5: dom (x |-- EV) = dom EV by A3, FINSEQ_3:29;

A6: Carrier (x |-- B) c= B by RLVECT_2:def 6;

(x |-- EV) . y = 0 ; :: thesis: x in Affin B

.= B by A1, XBOOLE_1:28 ;

hence x in Affin B by A2, A11, RLAFFIN1:75; :: thesis: verum

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

let V be RealLinearSpace; :: thesis: for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

let Affv be finite affinely-independent Subset of V; :: thesis: for EV being Enumeration of Affv

for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

let EV be Enumeration of Affv; :: thesis: for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

let B be Subset of V; :: thesis: ( B c= Affv & x in Affin Affv implies ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds

(x |-- EV) . y = 0 ) )

assume A1: B c= Affv ; :: thesis: ( not x in Affin Affv or ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds

(x |-- EV) . y = 0 ) )

set xA = x |-- Affv;

set xB = x |-- B;

set cA = card Affv;

set E = EV;

assume A2: x in Affin Affv ; :: thesis: ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds

(x |-- EV) . y = 0 )

set xE = x |-- EV;

A3: len (x |-- EV) = card Affv by Th16;

A4: rng EV = Affv by Def1;

then len EV = card Affv by FINSEQ_4:62;

then A5: dom (x |-- EV) = dom EV by A3, FINSEQ_3:29;

A6: Carrier (x |-- B) c= B by RLVECT_2:def 6;

hereby :: thesis: ( ( for y being set st y in dom (x |-- EV) & not EV . y in B holds

(x |-- EV) . y = 0 ) implies x in Affin B )

assume A10:
for y being set st y in dom (x |-- EV) & not EV . y in B holds (x |-- EV) . y = 0 ) implies x in Affin B )

assume
x in Affin B
; :: thesis: for y being set st y in dom (x |-- EV) & not EV . y in B holds

(x |-- EV) . y = 0

then A7: x |-- B = x |-- Affv by A1, RLAFFIN1:77;

let y be set ; :: thesis: ( y in dom (x |-- EV) & not EV . y in B implies (x |-- EV) . y = 0 )

assume that

A8: y in dom (x |-- EV) and

A9: not EV . y in B ; :: thesis: (x |-- EV) . y = 0

y in dom EV by A8, FUNCT_1:11;

then EV . y in Affv by A4, FUNCT_1:def 3;

then reconsider Ey = EV . y as Element of V ;

( (x |-- EV) . y = (x |-- Affv) . (EV . y) & not Ey in Carrier (x |-- B) ) by A6, A8, A9, FUNCT_1:12;

hence (x |-- EV) . y = 0 by A7, RLVECT_2:19; :: thesis: verum

end;(x |-- EV) . y = 0

then A7: x |-- B = x |-- Affv by A1, RLAFFIN1:77;

let y be set ; :: thesis: ( y in dom (x |-- EV) & not EV . y in B implies (x |-- EV) . y = 0 )

assume that

A8: y in dom (x |-- EV) and

A9: not EV . y in B ; :: thesis: (x |-- EV) . y = 0

y in dom EV by A8, FUNCT_1:11;

then EV . y in Affv by A4, FUNCT_1:def 3;

then reconsider Ey = EV . y as Element of V ;

( (x |-- EV) . y = (x |-- Affv) . (EV . y) & not Ey in Carrier (x |-- B) ) by A6, A8, A9, FUNCT_1:12;

hence (x |-- EV) . y = 0 by A7, RLVECT_2:19; :: thesis: verum

(x |-- EV) . y = 0 ; :: thesis: x in Affin B

A11: now :: thesis: for y being set st y in Affv \ B holds

(x |-- Affv) . y = 0

Affv \ (Affv \ B) =
Affv /\ B
by XBOOLE_1:48
(x |-- Affv) . y = 0

let y be set ; :: thesis: ( y in Affv \ B implies (x |-- Affv) . y = 0 )

assume A12: y in Affv \ B ; :: thesis: (x |-- Affv) . y = 0

then y in Affv by XBOOLE_0:def 5;

then consider z being object such that

A13: ( z in dom EV & EV . z = y ) by A4, FUNCT_1:def 3;

not y in B by A12, XBOOLE_0:def 5;

then (x |-- EV) . z = 0 by A5, A10, A13;

hence (x |-- Affv) . y = 0 by A5, A13, FUNCT_1:12; :: thesis: verum

end;assume A12: y in Affv \ B ; :: thesis: (x |-- Affv) . y = 0

then y in Affv by XBOOLE_0:def 5;

then consider z being object such that

A13: ( z in dom EV & EV . z = y ) by A4, FUNCT_1:def 3;

not y in B by A12, XBOOLE_0:def 5;

then (x |-- EV) . z = 0 by A5, A10, A13;

hence (x |-- Affv) . y = 0 by A5, A13, FUNCT_1:12; :: thesis: verum

.= B by A1, XBOOLE_1:28 ;

hence x in Affin B by A2, A11, RLAFFIN1:75; :: thesis: verum