let C, D be non empty set ; :: thesis: for c being Element of C
for f being one-to-one PartFunc of C,D st c in dom f holds
( c = (f ") /. (f /. c) & c = ((f ") * f) /. c )
let c be Element of C; :: thesis: for f being one-to-one PartFunc of C,D st c in dom f holds
( c = (f ") /. (f /. c) & c = ((f ") * f) /. c )
let f be one-to-one PartFunc of C,D; :: thesis: ( c in dom f implies ( c = (f ") /. (f /. c) & c = ((f ") * f) /. c ) )
assume A1: c in dom f ; :: thesis: ( c = (f ") /. (f /. c) & c = ((f ") * f) /. c )
hence A2: c = (f ") /. (f /. c) by Th11; :: thesis: c = ((f ") * f) /. c
f " = f " ;
then f /. c in rng f by A1, Th11;
then f /. c in dom (f ") by FUNCT_1:33;
hence c = ((f ") * f) /. c by A1, A2, Th4; :: thesis: verum