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:35, FUNCT_1:37;
hence ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d ) by A1, Th11, PARTFUN1:def 6; :: thesis: verum