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 )

( c in SC iff ( c in dom f & f /. c in X ) ) ; :: thesis: SC = f " X

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 A4:
for c being Element of C holds
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 )

A2: c in dom f and

A3: f /. c in X ; :: thesis: c in SC

f . c in X by A2, A3, PARTFUN1:def 6;

hence c in SC by A1, A2, FUNCT_1:def 7; :: thesis: verum

end;( 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 that
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 7;

hence ( c in dom f & f /. c in X ) by PARTFUN1:def 6; :: thesis: verum

end;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: verum

A2: c in dom f and

A3: f /. c in X ; :: thesis: c in SC

f . c in X by A2, A3, PARTFUN1:def 6;

hence c in SC by A1, A2, FUNCT_1:def 7; :: thesis: verum

( 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 ) )

hence
SC = f " X
by FUNCT_1:def 7; :: thesis: verum( ( 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 )

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 A6, A7, PARTFUN1:def 6;

hence x in SC by A4, A6; :: thesis: verum

end;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 that
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;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

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 A6, A7, PARTFUN1:def 6;

hence x in SC by A4, A6; :: thesis: verum