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 A1, FUNCT_1:def 6; :: thesis: verum