let X be set ; :: thesis: for D, C being non empty set
for SC being Subset of C
for f being PartFunc of C,D holds
( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )
let D, C be non empty set ; :: thesis: for SC being Subset of C
for f being PartFunc of C,D holds
( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )
let SC be Subset of C; :: thesis: for f being PartFunc of C,D holds
( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )
let f be PartFunc of C,D; :: thesis: ( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )
thus ( SC = f " X implies for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) ) :: thesis: ( ( for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) ) implies SC = f " X )

proof

assume A1: SC = f " X ; :: thesis: for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) )
let c be Element of C; :: thesis: ( c in SC iff ( c in dom f & f /. c in X ) )
thus ( c in SC implies ( c in dom f & f /. c in X ) ) :: thesis: ( c in dom f & f /. c in X implies c in SC )

proof

assume c in SC ; :: thesis: ( c in dom f & f /. c in X )
then ( c in dom f & f . c in X ) by A1, FUNCT_1:def 13;
hence ( c in dom f & f /. c in X ) by PARTFUN1:def 8; :: thesis: verum

end;

assume ( c in dom f & f /. c in X ) ; :: thesis: c in SC
then ( c in dom f & f . c in X ) by PARTFUN1:def 8;
hence c in SC by A1, FUNCT_1:def 13; :: thesis: verum

end;

assume A2: for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) ; :: thesis: SC = f " X

now

let x be set ; :: thesis: ( ( x in SC implies ( x in dom f & f . x in X ) ) & ( x in dom f & f . x in X implies x in SC ) )
thus ( x in SC implies ( x in dom f & f . x in X ) ) :: thesis: ( x in dom f & f . x in X implies x in SC )

proof

assume A3: x in SC ; :: thesis: ( x in dom f & f . x in X )
then reconsider x1 = x as Element of C ;
( x1 in dom f & f /. x1 in X ) by A2, A3;
hence ( x in dom f & f . x in X ) by PARTFUN1:def 8; :: thesis: verum

end;

assume A4: ( x in dom f & f . x in X ) ; :: thesis: x in SC
then reconsider x1 = x as Element of C ;
( x1 in dom f & f /. x1 in X ) by A4, PARTFUN1:def 8;
hence x in SC by A2; :: thesis: verum

end;

hence SC = f " X by FUNCT_1:def 13; :: thesis: verum