theorem Th13: :: PENCIL_1:13

for I being non empty set
for A being ManySortedSet of I holds
( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) )