let AFS be AffinSpace; :: thesis: for x being Element of AFS
for f being Permutation of the carrier of AFS
for A being Subset of AFS holds
( x in f .: A iff ex y being Element of AFS st
( y in A & f . y = x ) )

let x be Element of AFS; :: thesis: for f being Permutation of the carrier of AFS
for A being Subset of AFS holds
( x in f .: A iff ex y being Element of AFS st
( y in A & f . y = x ) )

let f be Permutation of the carrier of AFS; :: thesis: for A being Subset of AFS holds
( x in f .: A iff ex y being Element of AFS st
( y in A & f . y = x ) )

let A be Subset of AFS; :: thesis: ( x in f .: A iff ex y being Element of AFS st
( y in A & f . y = x ) )

thus ( x in f .: A implies ex y being Element of AFS st
( y in A & f . y = x ) ) :: thesis: ( ex y being Element of AFS st
( y in A & f . y = x ) implies x in f .: A )
proof
assume x in f .: A ; :: thesis: ex y being Element of AFS st
( y in A & f . y = x )

then ex y being object st
( y in dom f & y in A & x = f . y ) by FUNCT_1:def 6;
hence ex y being Element of AFS st
( y in A & f . y = x ) ; :: thesis: verum
end;
given y being Element of AFS such that A1: ( y in A & f . y = x ) ; :: thesis: x in f .: A
dom f = the carrier of AFS by FUNCT_2:52;
hence x in f .: A by ; :: thesis: verum