let X be set ; :: thesis: for p, q being XFinSequence
for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (q,(n + (card p))) c= X
let p, q be XFinSequence; :: thesis: for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (q,(n + (card p))) c= X
let n be Element of NAT ; :: thesis: ( Shift ((p ^ q),n) c= X implies Shift (q,(n + (card p))) c= X )
assume A1: Shift ((p ^ q),n) c= X ; :: thesis: Shift (q,(n + (card p))) c= X
Shift (q,(n + (card p))) c= Shift ((p ^ q),n) by Th85;
hence Shift (q,(n + (card p))) c= X by A1, XBOOLE_1:1; :: thesis: verum