let C, D, E be non empty set ; :: thesis: for c being Element of C
for f being PartFunc of C,D
for s being PartFunc of D,E st rng f c= dom s & c in dom f holds
(s * f) /. c = s /. (f /. c)
let c be Element of C; :: thesis: for f being PartFunc of C,D
for s being PartFunc of D,E st rng f c= dom s & c in dom f holds
(s * f) /. c = s /. (f /. c)
let f be PartFunc of C,D; :: thesis: for s being PartFunc of D,E st rng f c= dom s & c in dom f holds
(s * f) /. c = s /. (f /. c)
let s be PartFunc of D,E; :: thesis: ( rng f c= dom s & c in dom f implies (s * f) /. c = s /. (f /. c) )
assume A1: ( rng f c= dom s & c in dom f ) ; :: thesis: (s * f) /. c = s /. (f /. c)
then f /. c in rng f by Th4;
hence (s * f) /. c = s /. (f /. c) by A1, Th9; :: thesis: verum