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

( 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