let X, Y be non empty set ; :: thesis: for Z being set
for s being sequence of X
for h1 being PartFunc of ,
for h2 being PartFunc of , 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 ,
for h2 being PartFunc of , 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 ,
for h2 being PartFunc of , st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s
let h1 be PartFunc of ,; :: thesis: for h2 being PartFunc of , st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s
let h2 be PartFunc of ,; :: 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
A2: rng s c= dom h1 by A1, FUNCT_1:171;
h1 .: (rng s) c= dom h2 by A1, FUNCT_1:171;
then A3: rng (h1 /* s) c= dom h2 by A2, Th30;
s . n in rng s by Th28;
then A4: s . n in dom h1 by A1, FUNCT_1:21;
thus ((h2 * h1) /* s) . n = (h2 * h1) . (s . n) by A1, FUNCT_2:185
.= h2 . (h1 . (s . n)) by A4, FUNCT_1:23
.= h2 . ((h1 /* s) . n) by A2, FUNCT_2:185
.= (h2 /* (h1 /* s)) . n by A3, FUNCT_2:185 ; :: thesis: verum

end;

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