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 )

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

hence x 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 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

given y being Element of AFS such that A1:
( y in A & f . y = x )
; :: thesis: x in f .: A
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;( 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

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

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