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

now

let r be Element of Y; :: thesis: ( ( r in h .: (rng s) implies r in rng (h /* s) ) & ( r in rng (h /* s) implies r in h .: (rng s) ) )
thus ( r in h .: (rng s) implies r in rng (h /* s) ) :: thesis: ( r in rng (h /* s) implies r in h .: (rng s) )

proof

assume r in h .: (rng s) ; :: thesis: r in rng (h /* s)
then consider p being Element of X such that
A2: ( p in dom h & p in rng s & r = h . p ) by PARTFUN2:78;
consider n being Element of NAT such that
A3: p = s . n by A2, FUNCT_2:190;
r = (h /* s) . n by A1, A2, A3, FUNCT_2:185;
hence r in rng (h /* s) by Th28; :: thesis: verum

end;

assume r in rng (h /* s) ; :: thesis: r in h .: (rng s)
then consider n being Element of NAT such that
A4: (h /* s) . n = r by FUNCT_2:190;
A5: s . n in rng s by Th28;
r = h . (s . n) by A1, A4, FUNCT_2:185;
hence r in h .: (rng s) by A1, A5, FUNCT_1:def 12; :: thesis: verum

end;

hence h .: (rng s) = rng (h /* s) by SUBSET_1:8; :: thesis: verum