let X be set ; :: thesis: for p, q being XFinSequence
for n being 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 Nat st Shift ((p ^ q),n) c= X holds
Shift (q,(n + (card p))) c= X
let n be 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 Th78;
hence Shift (q,(n + (card p))) c= X by A1; :: thesis: verum