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

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