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

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