let D be non empty set ; :: thesis: for f1, f2 being FinSequence of D
for i being Element of NAT holds (f1 ^ f2) | ((len f1) + i) = f1 ^ (f2 | i)
let f1, f2 be FinSequence of D; :: thesis: for i being Element of NAT holds (f1 ^ f2) | ((len f1) + i) = f1 ^ (f2 | i)
let i be Element of NAT ; :: thesis: (f1 ^ f2) | ((len f1) + i) = f1 ^ (f2 | i)
A1: (f1 ^ f2) | ((len f1) + i) = (f1 ^ f2) | (Seg ((len f1) + i)) by FINSEQ_1:def 15;
f2 | i = f2 | (Seg i) by FINSEQ_1:def 15;
hence (f1 ^ f2) | ((len f1) + i) = f1 ^ (f2 | i) by A1, FINSEQ_6:16; :: thesis: verum