let A, B be non empty finite set ; :: thesis: ( A misses B implies ( (canFS A) ^ (canFS B) is one-to-one onto FinSequence of A \/ B & dom ((canFS A) ^ (canFS B)) = Seg (card (A \/ B)) ) )

assume A1: A misses B ; :: thesis: ( (canFS A) ^ (canFS B) is one-to-one onto FinSequence of A \/ B & dom ((canFS A) ^ (canFS B)) = Seg (card (A \/ B)) )

A2: rng (canFS A) = A by FUNCT_2:def 3;

A3: rng (canFS B) = B by FUNCT_2:def 3;

then A4: rng ((canFS A) ^ (canFS B)) = A \/ B by FINSEQ_1:31, A2;

then reconsider f = (canFS A) ^ (canFS B) as FinSequence of A \/ B by FINSEQ_1:def 4;

dom f = Seg ((len (canFS A)) + (len (canFS B))) by FINSEQ_1:def 7

.= Seg ((card A) + (len (canFS B))) by FINSEQ_1:93

.= Seg ((card A) + (card B)) by FINSEQ_1:93

.= Seg (card (A \/ B)) by A1, CARD_2:40 ;

hence ( (canFS A) ^ (canFS B) is one-to-one onto FinSequence of A \/ B & dom ((canFS A) ^ (canFS B)) = Seg (card (A \/ B)) ) by A2, FINSEQ_3:91, A1, A3, A4, FUNCT_2:def 3; :: thesis: verum

assume A1: A misses B ; :: thesis: ( (canFS A) ^ (canFS B) is one-to-one onto FinSequence of A \/ B & dom ((canFS A) ^ (canFS B)) = Seg (card (A \/ B)) )

A2: rng (canFS A) = A by FUNCT_2:def 3;

A3: rng (canFS B) = B by FUNCT_2:def 3;

then A4: rng ((canFS A) ^ (canFS B)) = A \/ B by FINSEQ_1:31, A2;

then reconsider f = (canFS A) ^ (canFS B) as FinSequence of A \/ B by FINSEQ_1:def 4;

dom f = Seg ((len (canFS A)) + (len (canFS B))) by FINSEQ_1:def 7

.= Seg ((card A) + (len (canFS B))) by FINSEQ_1:93

.= Seg ((card A) + (card B)) by FINSEQ_1:93

.= Seg (card (A \/ B)) by A1, CARD_2:40 ;

hence ( (canFS A) ^ (canFS B) is one-to-one onto FinSequence of A \/ B & dom ((canFS A) ^ (canFS B)) = Seg (card (A \/ B)) ) by A2, FINSEQ_3:91, A1, A3, A4, FUNCT_2:def 3; :: thesis: verum