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 A2: ( d = f . ((f " ) . d) & d = (f * (f " )) . d ) by FUNCT_1:57;
d in dom (f * (f " )) by A1, FUNCT_1:59;
hence ( d = f /. ((f " ) /. d) & d = (f * (f " )) /. d ) by A1, A2, Th18, PARTFUN1:def 8; :: thesis: verum