let k be Nat; :: thesis: for V being LinearTopSpace

for A being finite affinely-independent Subset of V

for E being Enumeration of A

for v being Point of V

for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let V be LinearTopSpace; :: thesis: for A being finite affinely-independent Subset of V

for E being Enumeration of A

for v being Point of V

for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let A be finite affinely-independent Subset of V; :: thesis: for E being Enumeration of A

for v being Point of V

for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let E be Enumeration of A; :: thesis: for v being Point of V

for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let v be Point of V; :: thesis: for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let Ev be Enumeration of v + A; :: thesis: ( Ev = E + ((card A) |-> v) implies for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } )

assume A1: Ev = E + ((card A) |-> v) ; :: thesis: for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

set T = transl (v,V);

let X be set ; :: thesis: (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

set U = { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } ;

set W = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } ;

A2: Affin (v + A) = v + (Affin A) by RLAFFIN1:53;

assume y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } ; :: thesis: y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) }

then consider w being Point of V such that

A9: y = w and

A10: w in Affin (v + A) and

A11: (w |-- Ev) | k in X ;

w in { (v + t) where t is Point of V : t in Affin A } by A2, A10, RUSUB_4:def 8;

then consider u being Point of V such that

A12: w = v + u and

A13: u in Affin A ;

w |-- Ev = u |-- E by A1, A12, A13, Th17;

then ( dom (transl (v,V)) = the carrier of V & u in { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } ) by A11, A13, FUNCT_2:52;

then (transl (v,V)) . u in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } by FUNCT_1:def 6;

hence y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } by A9, A12, RLTOPSP1:def 10; :: thesis: verum

for A being finite affinely-independent Subset of V

for E being Enumeration of A

for v being Point of V

for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let V be LinearTopSpace; :: thesis: for A being finite affinely-independent Subset of V

for E being Enumeration of A

for v being Point of V

for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let A be finite affinely-independent Subset of V; :: thesis: for E being Enumeration of A

for v being Point of V

for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let E be Enumeration of A; :: thesis: for v being Point of V

for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let v be Point of V; :: thesis: for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

let Ev be Enumeration of v + A; :: thesis: ( Ev = E + ((card A) |-> v) implies for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } )

assume A1: Ev = E + ((card A) |-> v) ; :: thesis: for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

set T = transl (v,V);

let X be set ; :: thesis: (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

set U = { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } ;

set W = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } ;

A2: Affin (v + A) = v + (Affin A) by RLAFFIN1:53;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } c= (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) }

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } or y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } )let y be object ; :: thesis: ( y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } implies y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } )

assume y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } ; :: thesis: y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

then consider x being object such that

x in dom (transl (v,V)) and

A3: x in { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } and

A4: (transl (v,V)) . x = y by FUNCT_1:def 6;

consider u being Point of V such that

A5: x = u and

A6: u in Affin A and

A7: (u |-- E) | k in X by A3;

v + u in { (v + t) where t is Point of V : t in Affin A } by A6;

then A8: v + u in Affin (v + A) by A2, RUSUB_4:def 8;

u |-- E = (v + u) |-- Ev by A1, A6, Th17;

then v + u in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } by A7, A8;

hence y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } by A4, A5, RLTOPSP1:def 10; :: thesis: verum

end;assume y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } ; :: thesis: y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

then consider x being object such that

x in dom (transl (v,V)) and

A3: x in { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } and

A4: (transl (v,V)) . x = y by FUNCT_1:def 6;

consider u being Point of V such that

A5: x = u and

A6: u in Affin A and

A7: (u |-- E) | k in X by A3;

v + u in { (v + t) where t is Point of V : t in Affin A } by A6;

then A8: v + u in Affin (v + A) by A2, RUSUB_4:def 8;

u |-- E = (v + u) |-- Ev by A1, A6, Th17;

then v + u in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } by A7, A8;

hence y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } by A4, A5, RLTOPSP1:def 10; :: thesis: verum

assume y in { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) } ; :: thesis: y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) }

then consider w being Point of V such that

A9: y = w and

A10: w in Affin (v + A) and

A11: (w |-- Ev) | k in X ;

w in { (v + t) where t is Point of V : t in Affin A } by A2, A10, RUSUB_4:def 8;

then consider u being Point of V such that

A12: w = v + u and

A13: u in Affin A ;

w |-- Ev = u |-- E by A1, A12, A13, Th17;

then ( dom (transl (v,V)) = the carrier of V & u in { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } ) by A11, A13, FUNCT_2:52;

then (transl (v,V)) . u in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } by FUNCT_1:def 6;

hence y in (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } by A9, A12, RLTOPSP1:def 10; :: thesis: verum