let p, q be XFinSequence; for n being Nat holds Shift (q,(n + (card p))) c= Shift ((p ^ q),n)
let n be Nat; Shift (q,(n + (card p))) c= Shift ((p ^ q),n)
A1:
Shift ((Shift (q,(card p))),n) = Shift (q,(n + (card p)))
by VALUED_1:21;
p ^ q = p +* (Shift (q,(card p)))
by Th74;
then
Shift ((p ^ q),n) = (Shift (p,n)) +* (Shift ((Shift (q,(card p))),n))
by VALUED_1:23;
hence
Shift (q,(n + (card p))) c= Shift ((p ^ q),n)
by A1, FUNCT_4:25; verum