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 :: thesis: for n being Element of NAT holds ((h2 * h1) /* s) . n = (h2 /* (h1 /* s)) . n

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:101;
h1 .: (rng s) c= dom h2 by A1, FUNCT_1:101;
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:11;
thus ((h2 * h1) /* s) . n = (h2 * h1) . (s . n) by A1, FUNCT_2:108
.= h2 . (h1 . (s . n)) by A4, FUNCT_1:13
.= h2 . ((h1 /* s) . n) by A2, FUNCT_2:108
.= (h2 /* (h1 /* s)) . n by A3, FUNCT_2:108 ; :: thesis: verum

end;

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