let C, D be non empty set ; :: thesis: for c being Element of C

for d being Element of D

for f being PartFunc of C,D holds

( ( c in dom f & d = f /. c ) iff [c,d] in f )

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

for f being PartFunc of C,D holds

( ( c in dom f & d = f /. c ) iff [c,d] in f )

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

( ( c in dom f & d = f /. c ) iff [c,d] in f )

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

thus ( c in dom f & d = f /. c implies [c,d] in f ) :: thesis: ( [c,d] in f implies ( c in dom f & d = f /. c ) )

then ( c in dom f & d = f . c ) by FUNCT_1:1;

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

for d being Element of D

for f being PartFunc of C,D holds

( ( c in dom f & d = f /. c ) iff [c,d] in f )

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

for f being PartFunc of C,D holds

( ( c in dom f & d = f /. c ) iff [c,d] in f )

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

( ( c in dom f & d = f /. c ) iff [c,d] in f )

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

thus ( c in dom f & d = f /. c implies [c,d] in f ) :: thesis: ( [c,d] in f implies ( c in dom f & d = f /. c ) )

proof

assume
[c,d] in f
; :: thesis: ( c in dom f & d = f /. c )
assume that

A1: c in dom f and

A2: d = f /. c ; :: thesis: [c,d] in f

d = f . c by A1, A2, PARTFUN1:def 6;

hence [c,d] in f by A1, FUNCT_1:1; :: thesis: verum

end;A1: c in dom f and

A2: d = f /. c ; :: thesis: [c,d] in f

d = f . c by A1, A2, PARTFUN1:def 6;

hence [c,d] in f by A1, FUNCT_1:1; :: thesis: verum

then ( c in dom f & d = f . c ) by FUNCT_1:1;

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