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

proof

assume ( c in dom f & d = f /. c ) ; :: thesis: [c,d] in f
then ( c in dom f & d = f . c ) by PARTFUN1:def 8;
hence [c,d] in f by FUNCT_1:8; :: thesis: verum

end;

assume [c,d] in f ; :: thesis: ( c in dom f & d = f /. c )
then ( c in dom f & d = f . c ) by FUNCT_1:8;
hence ( c in dom f & d = f /. c ) by PARTFUN1:def 8; :: thesis: verum