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;

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 ; :: 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;

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 ) } )
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