let p, q be XFinSequence; :: thesis: ( p ^ q = {} implies ( p = {} & q = {} ) )
assume p ^ q = {} ; :: thesis: ( p = {} & q = {} )
then 0 = len (p ^ q)
.= (len p) + (len q) by Def3 ;
hence ( p = {} & q = {} ) ; :: thesis: verum