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 that
A1: rng f c= dom s and
A2: c in dom f ; :: thesis: (s * f) /. c = s /. (f /. c)
f /. c in rng f by A2, Th2;
hence (s * f) /. c = s /. (f /. c) by A1, A2, Th4; :: thesis: verum