let D, E, C be non empty set ; :: thesis:
let f be PartFunc of C,D; :: thesis:
let s be PartFunc of D,E; :: thesis:
let h be PartFunc of C,E; :: thesis:
thus ( h = s * f implies ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) ) ) :: thesis:

assume A1: h = s * f ; :: thesis:

A2: now

let c be Element of C; :: thesis:
thus ( c in dom h implies ( c in dom f & f /. c in dom s ) ) :: thesis:

assume c in dom h ; :: thesis:
then ( c in dom f & f . c in dom s ) by A1, FUNCT_1:21;
hence ( c in dom f & f /. c in dom s ) by PARTFUN1:def 8; :: thesis:

end;

assume ( c in dom f & f /. c in dom s ) ; :: thesis:
then ( c in dom f & f . c in dom s ) by PARTFUN1:def 8;
hence c in dom h by A1, FUNCT_1:21; :: thesis:

end;

hence for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ; :: thesis:
let c be Element of C; :: thesis:
assume A3: c in dom h ; :: thesis:
then h . c = s . (f . c) by A1, FUNCT_1:22;
then A4: h /. c = s . (f . c) by A3, PARTFUN1:def 8;
A5: ( c in dom f & f /. c in dom s ) by A2, A3;
then h /. c = s . (f /. c) by A4, PARTFUN1:def 8;
hence h /. c = s /. (f /. c) by A5, PARTFUN1:def 8; :: thesis:

end;

assume that
A6: for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) and
A7: for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ; :: thesis:

A8: now

let x be set ; :: thesis:
thus ( x in dom h implies ( x in dom f & f . x in dom s ) ) :: thesis:

assume A9: x in dom h ; :: thesis:
then reconsider y = x as Element of C ;
( y in dom f & f /. y in dom s ) by A6, A9;
hence ( x in dom f & f . x in dom s ) by PARTFUN1:def 8; :: thesis:

end;

thus ( x in dom f & f . x in dom s implies x in dom h ) :: thesis:

assume A10: ( x in dom f & f . x in dom s ) ; :: thesis:
then reconsider y = x as Element of C ;
( y in dom f & f /. y in dom s ) by A10, PARTFUN1:def 8;
hence x in dom h by A6; :: thesis:

end;

now

let x be set ; :: thesis:
assume A11: x in dom h ; :: thesis:
then reconsider y = x as Element of C ;
A12: ( y in dom f & f /. y in dom s ) by A6, A11;
h /. y = s /. (f /. y) by A7, A11;
then h . y = s /. (f /. y) by A11, PARTFUN1:def 8;
then h . x = s . (f /. y) by A12, PARTFUN1:def 8;
hence h . x = s . (f . x) by A12, PARTFUN1:def 8; :: thesis:

end;

hence h = s * f by A8, FUNCT_1:20; :: thesis: