let i, j be Element of NAT ; :: thesis: for q being FinSubsequence holds (i + j) Shift q = i Shift (j Shift q)
let q be FinSubsequence; :: thesis: (i + j) Shift q = i Shift (j Shift q)
set Sj = j Shift q;
set Sij = (i + j) Shift q;
set Si = i Shift (j Shift q);
set Xj = { (j + k) where k is Element of NAT : k in dom q } ;
set Xi = { (i + k) where k is Element of NAT : k in dom (j Shift q) } ;
set Xij = { ((i + j) + k) where k is Element of NAT : k in dom q } ;
A1: dom (j Shift q) = { (j + k) where k is Element of NAT : k in dom q } by Def15;
A2: dom (i Shift (j Shift q)) = { (i + k) where k is Element of NAT : k in dom (j Shift q) } by Def15;
A3: dom ((i + j) Shift q) = { ((i + j) + k) where k is Element of NAT : k in dom q } by Def15;
A4: { (i + k) where k is Element of NAT : k in dom (j Shift q) } = { ((i + j) + k) where k is Element of NAT : k in dom q }

proof

thus { (i + k) where k is Element of NAT : k in dom (j Shift q) } c= { ((i + j) + k) where k is Element of NAT : k in dom q } :: according to XBOOLE_0:def 10 :: thesis: { ((i + j) + k) where k is Element of NAT : k in dom q } c= { (i + k) where k is Element of NAT : k in dom (j Shift q) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (i + k) where k is Element of NAT : k in dom (j Shift q) } or x in { ((i + j) + k) where k is Element of NAT : k in dom q } )
assume x in { (i + k) where k is Element of NAT : k in dom (j Shift q) } ; :: thesis: x in { ((i + j) + k) where k is Element of NAT : k in dom q }
then consider k being Element of NAT such that
A5: x = i + k and
A6: k in dom (j Shift q) ;
dom (j Shift q) = { (j + K) where K is Element of NAT : K in dom q } by Def15;
then consider K being Element of NAT such that
A7: k = j + K and
A8: K in dom q by A6;
x = (i + j) + K by A5, A7;
hence x in { ((i + j) + k) where k is Element of NAT : k in dom q } by A8; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((i + j) + k) where k is Element of NAT : k in dom q } or x in { (i + k) where k is Element of NAT : k in dom (j Shift q) } )
assume x in { ((i + j) + k) where k is Element of NAT : k in dom q } ; :: thesis: x in { (i + k) where k is Element of NAT : k in dom (j Shift q) }
then consider k being Element of NAT such that
A9: x = (i + j) + k and
A10: k in dom q ;
reconsider K = j + k as Element of NAT ;
A11: dom (j Shift q) = { (j + l) where l is Element of NAT : l in dom q } by Def15;
A12: x = i + K by A9;
K in dom (j Shift q) by A10, A11;
hence x in { (i + k) where k is Element of NAT : k in dom (j Shift q) } by A12; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in { ((i + j) + k) where k is Element of NAT : k in dom q } implies ((i + j) Shift q) . x = (i Shift (j Shift q)) . x )
assume x in { ((i + j) + k) where k is Element of NAT : k in dom q } ; :: thesis: ((i + j) Shift q) . x = (i Shift (j Shift q)) . x
then consider k being Element of NAT such that
A13: x = (i + j) + k and
A14: k in dom q ;
A15: x = i + (j + k) by A13;
A16: j + k in dom (j Shift q) by A1, A14;
thus ((i + j) Shift q) . x = q . k by A13, A14, Def15
.= (j Shift q) . (j + k) by A14, Def15
.= (i Shift (j Shift q)) . x by A15, A16, Def15 ; :: thesis: verum

end;

hence (i + j) Shift q = i Shift (j Shift q) by A2, A3, A4, FUNCT_1:2; :: thesis: verum