let X be set ; :: thesis: for p, q being XFinSequence
for n being Nat st Shift ((p ^ q),n) c= X holds
Shift (p,n) c= X
let p, q be XFinSequence; :: thesis: for n being Nat st Shift ((p ^ q),n) c= X holds
Shift (p,n) c= X
let n be Nat; :: thesis: ( Shift ((p ^ q),n) c= X implies Shift (p,n) c= X )
assume A1: Shift ((p ^ q),n) c= X ; :: thesis: Shift (p,n) c= X
Shift (p,n) c= Shift ((p ^ q),n) by Th77;
hence Shift (p,n) c= X by A1; :: thesis: verum