let X be set ; :: thesis: for C, D 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 C, D 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 ;
hence ( c in dom f & f /. c in X ) by PARTFUN1:def 6; :: thesis: verum
end;
assume that
A2: c in dom f and
A3: f /. c in X ; :: thesis: c in SC
f . c in X by ;
hence c in SC by ; :: thesis: verum
end;
assume A4: for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) ; :: thesis: SC = f " X
now :: thesis: for x being object holds
( ( x in SC implies ( x in dom f & f . x in X ) ) & ( x in dom f & f . x in X implies x in SC ) )
let x be object ; :: 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 A5: 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 A4, A5;
hence ( x in dom f & f . x in X ) by PARTFUN1:def 6; :: thesis: verum
end;
assume that
A6: x in dom f and
A7: f . x in X ; :: thesis: x in SC
reconsider x1 = x as Element of C by A6;
f /. x1 in X by ;
hence x in SC by A4, A6; :: thesis: verum
end;
hence SC = f " X by FUNCT_1:def 7; :: thesis: verum