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