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 f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )

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

for f being PartFunc of C,D holds

( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )

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

( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )

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

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

A4: [c,(f /. c)] in f and

A5: f /. c in SD ; :: thesis: c in f " SD

c in dom f by A4, Th46;

hence c in f " SD by A5, Th26; :: thesis: verum

for c being Element of C

for f being PartFunc of C,D holds

( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )

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

for f being PartFunc of C,D holds

( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )

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

( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )

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

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

proof

assume that
assume A1:
c in f " SD
; :: thesis: ( [c,(f /. c)] in f & f /. c in SD )

then A2: f . c in SD by GRFUNC_1:26;

A3: [c,(f . c)] in f by A1, GRFUNC_1:26;

then c in dom f by FUNCT_1:1;

hence ( [c,(f /. c)] in f & f /. c in SD ) by A3, A2, PARTFUN1:def 6; :: thesis: verum

end;then A2: f . c in SD by GRFUNC_1:26;

A3: [c,(f . c)] in f by A1, GRFUNC_1:26;

then c in dom f by FUNCT_1:1;

hence ( [c,(f /. c)] in f & f /. c in SD ) by A3, A2, PARTFUN1:def 6; :: thesis: verum

A4: [c,(f /. c)] in f and

A5: f /. c in SD ; :: thesis: c in f " SD

c in dom f by A4, Th46;

hence c in f " SD by A5, Th26; :: thesis: verum