consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
consider m being Nat such that
A2: dom g = Seg m by FINSEQ_1:def 2;
A3: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;

per cases ( m <= n or m > n ) ;

suppose A4: m <= n ; :: thesis: f +* g is FinSequence-like

take n ; :: according to FINSEQ_1:def 2 :: thesis: dom (f +* g) = Seg n
thus dom (f +* g) = Seg n by A1, A2, A3, A4, XBOOLE_1:12, FINSEQ_1:5; :: thesis: verum

end;

suppose A5: m > n ; :: thesis: f +* g is FinSequence-like

take m ; :: according to FINSEQ_1:def 2 :: thesis: dom (f +* g) = Seg m
thus dom (f +* g) = Seg m by A1, A2, A3, A5, XBOOLE_1:12, FINSEQ_1:5; :: thesis: verum

end;

end;