theorem :: FINSEQ_3:162

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