(f ^ g) | (dom f) = (f ^ g) | (Seg (len f)) by FINSEQ_1:def 3;
hence (f ^ g) | (len f) = f ; :: thesis: verum