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