let q, p be XFinSequence; :: thesis: for n being Element of NAT holds Shift (q,(n + (card p))) c= Shift ((p ^ q),n)
let n be Element of NAT ; :: thesis: Shift (q,(n + (card p))) c= Shift ((p ^ q),n)
A: Shift ((Shift (q,(card p))),n) = Shift (q,(n + (card p))) by VALUED_1:22;
p ^ q = p +* (Shift (q,(card p))) by Th81;
then Shift ((p ^ q),n) = (Shift (p,n)) +* (Shift ((Shift (q,(card p))),n)) by VALUED_1:24;
hence Shift (q,(n + (card p))) c= Shift ((p ^ q),n) by A, FUNCT_4:26; :: thesis: verum