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;

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 )
;

end;

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;thus dom (f +* g) = Seg n by A1, A2, A3, A4, XBOOLE_1:12, FINSEQ_1:5; :: thesis: verum

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;thus dom (f +* g) = Seg m by A1, A2, A3, A5, XBOOLE_1:12, FINSEQ_1:5; :: thesis: verum