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 :: thesis: for r being Element of Y holds
( ( r in h .: (rng s) implies r in rng (h /* s) ) & ( r in rng (h /* s) implies r in h .: (rng s) ) )
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
p in dom h and
A2: p in rng s and
A3: r = h . p by PARTFUN2:59;
consider n being Element of NAT such that
A4: p = s . n by A2, FUNCT_2:113;
r = (h /* s) . n by A1, A3, A4, FUNCT_2:108;
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
A5: (h /* s) . n = r by FUNCT_2:113;
A6: s . n in rng s by Th28;
r = h . (s . n) by A1, A5, FUNCT_2:108;
hence r in h .: (rng s) by A1, A6, FUNCT_1:def 6; :: thesis: verum
end;
hence h .: (rng s) = rng (h /* s) by SUBSET_1:3; :: thesis: verum