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

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