let X be set ; :: thesis:
let C, D be non empty set ; :: thesis:
let SC be Subset of C; :: thesis:
let f be PartFunc of C,D; :: thesis:
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:

proof

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

proof

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

end;

assume that
A2: c in dom f and
A3: f /. c in X ; :: thesis:
f . c in X by A2, A3, PARTFUN1:def 6;
hence c in SC by A1, A2, FUNCT_1:def 7; :: thesis:

end;

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

now :: thesis:

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

proof

assume A5: x in SC ; :: thesis:
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:

end;

assume that
A6: x in dom f and
A7: f . x in X ; :: thesis:
reconsider x1 = x as Element of C by A6;
f /. x1 in X by A6, A7, PARTFUN1:def 6;
hence x in SC by A4, A6; :: thesis:

end;

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