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)
( (f1 ^ f2) | ((len f1) + i) = (f1 ^ f2) | (Seg ((len f1) + i)) & f2 | i = f2 | (Seg i) ) by FINSEQ_1:def 16;
hence (f1 ^ f2) | ((len f1) + i) = f1 ^ (f2 | i) by FINSEQ_6:14; :: thesis: verum