let p, q be XFinSequence; :: thesis: for n being Nat holds Shift (p,n) c= Shift ((p ^ q),n)
let n be Nat; :: thesis: Shift (p,n) c= Shift ((p ^ q),n)
p ^ q = p +* (Shift (q,(card p))) by Th74;
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 Th76;
hence Shift (p,n) c= Shift ((p ^ q),n) by A1, FUNCT_4:32; :: thesis: verum