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 c in dom f & f /. c in dom s 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 c in dom f & f /. c in dom s holds
(s * f) /. c = s /. (f /. c)
let f be PartFunc of C,D; :: thesis: for s being PartFunc of D,E st c in dom f & f /. c in dom s holds
(s * f) /. c = s /. (f /. c)
let s be PartFunc of D,E; :: thesis: ( c in dom f & f /. c in dom s implies (s * f) /. c = s /. (f /. c) )
assume ( c in dom f & f /. c in dom s ) ; :: thesis: (s * f) /. c = s /. (f /. c)
then c in dom (s * f) by Th3;
hence (s * f) /. c = s /. (f /. c) by Th3; :: thesis: verum