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 Nat such that
A2: dom f = Seg n by FINSEQ_1:def 2;
consider m being Nat 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: dom h = Seg n
thus dom h = Seg n by A1, A2, A3, A4, FINSEQ_1:7; :: thesis: verum
end;
suppose A5: m <= n ; :: thesis: h is FinSequence-like
take m ; :: according to FINSEQ_1:def 2 :: thesis: dom h = Seg m
thus dom h = Seg m by A1, A2, A3, A5, FINSEQ_1:7; :: thesis: verum
end;
end;
end;
hence h is FinSequence ; :: thesis: verum