let A, B be set ; :: thesis: for F, G being FinSequence st F is one-to-one & G is one-to-one & A /\ B = {} & rng F = A & rng G = B holds
( F ^ G is one-to-one & dom (F ^ G) = Seg ((len F) + (len G)) & rng (F ^ G) = (rng F) \/ (rng G) )
let F, G be FinSequence; :: thesis: ( F is one-to-one & G is one-to-one & A /\ B = {} & rng F = A & rng G = B implies ( F ^ G is one-to-one & dom (F ^ G) = Seg ((len F) + (len G)) & rng (F ^ G) = (rng F) \/ (rng G) ) )
assume that
A1: F is one-to-one and
A2: G is one-to-one and
A3: A /\ B = {} and
A4: ( rng F = A & rng G = B ) ; :: thesis: ( F ^ G is one-to-one & dom (F ^ G) = Seg ((len F) + (len G)) & rng (F ^ G) = (rng F) \/ (rng G) )
dom (F ^ G) = Seg (len (F ^ G)) by FINSEQ_1:def 3
.= Seg ((len F) + (len G)) by FINSEQ_1:22 ;
hence ( F ^ G is one-to-one & dom (F ^ G) = Seg ((len F) + (len G)) & rng (F ^ G) = (rng F) \/ (rng G) ) by A1, A2, A3, A4, FINSEQ_1:31, FINSEQ_3:91, XBOOLE_0:def 7; :: thesis: verum