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 )
f " = f " ;
then A2: ( f /. c in rng f & c = (f " ) /. (f /. c) ) by A1, Th18;
thus A3: c = (f " ) /. (f /. c) by A1, Th18; :: thesis: c = ((f " ) * f) /. c
( f /. c in dom (f " ) & c in dom f ) by A1, A2, FUNCT_1:55;
hence c = ((f " ) * f) /. c by A3, Th9; :: thesis: verum