theorem Th7: :: BOOLMARK:7

for D being non empty set
for Q0, Q1 being FinSequence of D
for i being Element of NAT st 1 <= i & i <= len Q0 holds
(Q0 ^ Q1) /. i = Q0 /. i