let f, g be FinSequence; :: thesis: for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence
let h be Function; :: thesis: ( dom h = (dom f) /\ (dom g) implies h is FinSequence )
assume A1: dom h = (dom f) /\ (dom g) ; :: thesis: h is FinSequence
consider n being natural number such that
A2: dom f = Seg n by FINSEQ_1:def 2;
consider m being natural number such that
A3: dom g = Seg m by FINSEQ_1:def 2;
h is FinSequence-like

proof

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

suppose A4: n <= m ; :: thesis: h is FinSequence-like

take n ; :: according to FINSEQ_1:def 2 :: thesis: proj1 h = Seg n
thus proj1 h = Seg n by A1, A2, A3, A4, FINSEQ_1:9; :: thesis: verum

end;

suppose A5: m <= n ; :: thesis: h is FinSequence-like

take m ; :: according to FINSEQ_1:def 2 :: thesis: proj1 h = Seg m
thus proj1 h = Seg m by A1, A2, A3, A5, FINSEQ_1:9; :: thesis: verum

end;

end;

end;

hence h is FinSequence ; :: thesis: verum