let X, Y be non empty set ; :: thesis: for Z being set
for s being sequence of X
for h1 being PartFunc of X,Y
for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s
let Z be set ; :: thesis: for s being sequence of X
for h1 being PartFunc of X,Y
for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s
let s be sequence of X; :: thesis: for h1 being PartFunc of X,Y
for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s
let h1 be PartFunc of X,Y; :: thesis: for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s
let h2 be PartFunc of Y,Z; :: thesis: ( rng s c= dom (h2 * h1) implies h2 /* (h1 /* s) = (h2 * h1) /* s )
assume A1: rng s c= dom (h2 * h1) ; :: thesis: h2 /* (h1 /* s) = (h2 * h1) /* s

now

let n be Element of NAT ; :: thesis: ((h2 * h1) /* s) . n = (h2 /* (h1 /* s)) . n
s . n in rng s by Th28;
then A2: ( s . n in dom h1 & h1 . (s . n) in dom h2 ) by A1, FUNCT_1:21;
A3: ( rng s c= dom h1 & h1 .: (rng s) c= dom h2 ) by A1, FUNCT_1:171;
then A4: ( rng s c= dom h1 & rng (h1 /* s) c= dom h2 ) by Th38;
thus ((h2 * h1) /* s) . n = (h2 * h1) . (s . n) by A1, FUNCT_2:185
.= h2 . (h1 . (s . n)) by A2, FUNCT_1:23
.= h2 . ((h1 /* s) . n) by A3, FUNCT_2:185
.= (h2 /* (h1 /* s)) . n by A4, FUNCT_2:185 ; :: thesis: verum

end;

hence h2 /* (h1 /* s) = (h2 * h1) /* s by FUNCT_2:113; :: thesis: verum