let X be set ; :: thesis: for C, D being non empty set

for SD being Subset of D

for f being PartFunc of C,D holds

( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

let C, D be non empty set ; :: thesis: for SD being Subset of D

for f being PartFunc of C,D holds

( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

let SD be Subset of D; :: thesis: for f being PartFunc of C,D holds

( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

let f be PartFunc of C,D; :: thesis: ( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

thus ( SD = f .: X implies for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) ) :: thesis: ( ( for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) ) implies SD = f .: X )

A7: for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) and

A8: SD <> f .: X ; :: thesis: contradiction

consider x being object such that

A9: ( ( x in SD & not x in f .: X ) or ( x in f .: X & not x in SD ) ) by A8, TARSKI:2;

for SD being Subset of D

for f being PartFunc of C,D holds

( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

let C, D be non empty set ; :: thesis: for SD being Subset of D

for f being PartFunc of C,D holds

( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

let SD be Subset of D; :: thesis: for f being PartFunc of C,D holds

( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

let f be PartFunc of C,D; :: thesis: ( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

thus ( SD = f .: X implies for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) ) :: thesis: ( ( for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) ) implies SD = f .: X )

proof

assume that
assume A1:
SD = f .: X
; :: thesis: for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) )

let d be Element of D; :: thesis: ( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) )

thus ( d in SD implies ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) :: thesis: ( ex c being Element of C st

( c in dom f & c in X & d = f /. c ) implies d in SD )

A6: ( c in X & d = f /. c ) ; :: thesis: d in SD

f /. c = f . c by A5, PARTFUN1:def 6;

hence d in SD by A1, A5, A6, FUNCT_1:def 6; :: thesis: verum

end;( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) )

let d be Element of D; :: thesis: ( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) )

thus ( d in SD implies ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) :: thesis: ( ex c being Element of C st

( c in dom f & c in X & d = f /. c ) implies d in SD )

proof

given c being Element of C such that A5:
c in dom f
and
assume
d in SD
; :: thesis: ex c being Element of C st

( c in dom f & c in X & d = f /. c )

then consider x being object such that

A2: x in dom f and

A3: x in X and

A4: d = f . x by A1, FUNCT_1:def 6;

reconsider x = x as Element of C by A2;

take x ; :: thesis: ( x in dom f & x in X & d = f /. x )

thus ( x in dom f & x in X ) by A2, A3; :: thesis: d = f /. x

thus d = f /. x by A2, A4, PARTFUN1:def 6; :: thesis: verum

end;( c in dom f & c in X & d = f /. c )

then consider x being object such that

A2: x in dom f and

A3: x in X and

A4: d = f . x by A1, FUNCT_1:def 6;

reconsider x = x as Element of C by A2;

take x ; :: thesis: ( x in dom f & x in X & d = f /. x )

thus ( x in dom f & x in X ) by A2, A3; :: thesis: d = f /. x

thus d = f /. x by A2, A4, PARTFUN1:def 6; :: thesis: verum

A6: ( c in X & d = f /. c ) ; :: thesis: d in SD

f /. c = f . c by A5, PARTFUN1:def 6;

hence d in SD by A1, A5, A6, FUNCT_1:def 6; :: thesis: verum

A7: for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) and

A8: SD <> f .: X ; :: thesis: contradiction

consider x being object such that

A9: ( ( x in SD & not x in f .: X ) or ( x in f .: X & not x in SD ) ) by A8, TARSKI:2;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ( x in SD & not x in f .: X ) or ( x in f .: X & not x in SD ) )
by A9;

end;

suppose A10:
( x in SD & not x in f .: X )
; :: thesis: contradiction

then reconsider x = x as Element of D ;

consider c being Element of C such that

A11: c in dom f and

A12: c in X and

A13: x = f /. c by A7, A10;

x = f . c by A11, A13, PARTFUN1:def 6;

hence contradiction by A10, A11, A12, FUNCT_1:def 6; :: thesis: verum

end;consider c being Element of C such that

A11: c in dom f and

A12: c in X and

A13: x = f /. c by A7, A10;

x = f . c by A11, A13, PARTFUN1:def 6;

hence contradiction by A10, A11, A12, FUNCT_1:def 6; :: thesis: verum

suppose A14:
( x in f .: X & not x in SD )
; :: thesis: contradiction

then consider y being object such that

A15: y in dom f and

A16: y in X and

A17: x = f . y by FUNCT_1:def 6;

reconsider y = y as Element of C by A15;

x = f /. y by A15, A17, PARTFUN1:def 6;

hence contradiction by A7, A14, A15, A16; :: thesis: verum

end;A15: y in dom f and

A16: y in X and

A17: x = f . y by FUNCT_1:def 6;

reconsider y = y as Element of C by A15;

x = f /. y by A15, A17, PARTFUN1:def 6;

hence contradiction by A7, A14, A15, A16; :: thesis: verum