let X, Y be non empty set ; :: thesis: for s, s1 being sequence of X
for h being PartFunc of X,Y st rng s c= dom h & s1 is subsequence of s holds
h /* s1 is subsequence of h /* s
let s, s1 be sequence of X; :: thesis: for h being PartFunc of X,Y st rng s c= dom h & s1 is subsequence of s holds
h /* s1 is subsequence of h /* s
let h be PartFunc of X,Y; :: thesis: ( rng s c= dom h & s1 is subsequence of s implies h /* s1 is subsequence of h /* s )
assume that
A1: rng s c= dom h and
A2: s1 is subsequence of s ; :: thesis: h /* s1 is subsequence of h /* s
consider N being increasing sequence of NAT such that
A3: s1 = s * N by A2, Def13;
take N ; :: according to VALUED_0:def 17 :: thesis: h /* s1 = (h /* s) * N
thus h /* s1 = (h /* s) * N by A1, A3, FUNCT_2:110; :: thesis: verum