let C, D, E 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:

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

end;

end;

end;

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

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

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

end;

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

assume that
A12: x in dom f and
A13: f . x in dom s ; :: thesis:
reconsider y = x as Element of C by A12;
f /. y in dom s by A12, A13, PARTFUN1:def 6;
hence x in dom h by A8, A12; :: thesis:

end;

end;