theorem :: FINSEQ_3:161

for X, Y being set holds disjoin <*X,Y*> = <*[:X,{1}:],[:Y,{2}:]*>