let C, D be non empty set ; :: thesis: for d being Element of D
for f being one-to-one PartFunc of C,D st d in rng f holds
( d = f /. ((f " ) /. d) & d = (f * (f " )) /. d )
let d be Element of D; :: thesis: for f being one-to-one PartFunc of C,D st d in rng f holds
( d = f /. ((f " ) /. d) & d = (f * (f " )) /. d )
let f be one-to-one PartFunc of C,D; :: thesis: ( d in rng f implies ( d = f /. ((f " ) /. d) & d = (f * (f " )) /. d ) )
assume A1: d in rng f ; :: thesis: ( d = f /. ((f " ) /. d) & d = (f * (f " )) /. d )
then ( d = (f * (f " )) . d & d in dom (f * (f " )) ) by FUNCT_1:57, FUNCT_1:59;
hence ( d = f /. ((f " ) /. d) & d = (f * (f " )) /. d ) by A1, Th18, PARTFUN1:def 8; :: thesis: verum