let p, q be XFinSequence; :: thesis: for n being Element of NAT holds Shift (p,n) c= Shift ((p ^ q),n)
let n be Element of NAT ; :: thesis: Shift (p,n) c= Shift ((p ^ q),n)
p ^ q = p +* (Shift (q,(card p))) by Th81;
then A1: Shift ((p ^ q),n) = (Shift (p,n)) +* (Shift ((Shift (q,(card p))),n)) by VALUED_1:23;
Shift ((Shift (q,(card p))),n) = Shift (q,(n + (card p))) by VALUED_1:21;
then dom (Shift (p,n)) misses dom (Shift ((Shift (q,(card p))),n)) by Th83;
hence Shift (p,n) c= Shift ((p ^ q),n) by A1, FUNCT_4:32; :: thesis: verum