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

for c being Element of C

for f being PartFunc of C,D holds

( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

let SD be Subset of D; :: thesis: for c being Element of C

for f being PartFunc of C,D holds

( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

let c be Element of C; :: thesis: for f being PartFunc of C,D holds

( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

let f be PartFunc of C,D; :: thesis: ( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

thus ( c in dom f & f /. c in SD implies [c,(f /. c)] in SD |` f ) :: thesis: ( [c,(f /. c)] in SD |` f implies ( c in dom f & f /. c in SD ) )

then c in dom (SD |` f) by FUNCT_1:1;

then ( c in dom f & f . c in SD ) by FUNCT_1:54;

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

for c being Element of C

for f being PartFunc of C,D holds

( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

let SD be Subset of D; :: thesis: for c being Element of C

for f being PartFunc of C,D holds

( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

let c be Element of C; :: thesis: for f being PartFunc of C,D holds

( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

let f be PartFunc of C,D; :: thesis: ( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

thus ( c in dom f & f /. c in SD implies [c,(f /. c)] in SD |` f ) :: thesis: ( [c,(f /. c)] in SD |` f implies ( c in dom f & f /. c in SD ) )

proof

assume
[c,(f /. c)] in SD |` f
; :: thesis: ( c in dom f & f /. c in SD )
assume that

A1: c in dom f and

A2: f /. c in SD ; :: thesis: [c,(f /. c)] in SD |` f

f . c in SD by A1, A2, PARTFUN1:def 6;

then [c,(f . c)] in SD |` f by A1, GRFUNC_1:24;

hence [c,(f /. c)] in SD |` f by A1, PARTFUN1:def 6; :: thesis: verum

end;A1: c in dom f and

A2: f /. c in SD ; :: thesis: [c,(f /. c)] in SD |` f

f . c in SD by A1, A2, PARTFUN1:def 6;

then [c,(f . c)] in SD |` f by A1, GRFUNC_1:24;

hence [c,(f /. c)] in SD |` f by A1, PARTFUN1:def 6; :: thesis: verum

then c in dom (SD |` f) by FUNCT_1:1;

then ( c in dom f & f . c in SD ) by FUNCT_1:54;

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