A1: dom (g ^ f) = Seg ((len g) + (len f)) by Def2;
A2: dom g = Seg (len g) by FINSEQ_1:def 3;
then dom g c= dom (g ^ f) by A1, NAT_1:12, FINSEQ_1:5;
then A3: dom g = (dom (g ^ f)) /\ (dom g) by XBOOLE_1:28;
for i being object st i in dom g holds
(g ^ f) . i = g . i by Def2;
hence (g ^ f) | (len g) = g by A2, A3, FUNCT_1:46; :: thesis: verum