let AFS be AffinSpace; :: thesis: for a being Element of AFS

for f being Permutation of the carrier of AFS

for A being Subset of AFS st a in A holds

f . a in f .: A

let a be Element of AFS; :: thesis: for f being Permutation of the carrier of AFS

for A being Subset of AFS st a in A holds

f . a in f .: A

let f be Permutation of the carrier of AFS; :: thesis: for A being Subset of AFS st a in A holds

f . a in f .: A

let A be Subset of AFS; :: thesis: ( a in A implies f . a in f .: A )

A1: dom f = the carrier of AFS by FUNCT_2:52;

assume a in A ; :: thesis: f . a in f .: A

hence f . a in f .: A by A1, FUNCT_1:def 6; :: thesis: verum

for f being Permutation of the carrier of AFS

for A being Subset of AFS st a in A holds

f . a in f .: A

let a be Element of AFS; :: thesis: for f being Permutation of the carrier of AFS

for A being Subset of AFS st a in A holds

f . a in f .: A

let f be Permutation of the carrier of AFS; :: thesis: for A being Subset of AFS st a in A holds

f . a in f .: A

let A be Subset of AFS; :: thesis: ( a in A implies f . a in f .: A )

A1: dom f = the carrier of AFS by FUNCT_2:52;

assume a in A ; :: thesis: f . a in f .: A

hence f . a in f .: A by A1, FUNCT_1:def 6; :: thesis: verum