theorem Th6: :: CALCUL_1:6

for fin, fin1 being FinSequence holds
( len fin <= len (fin ^ fin1) & len fin1 <= len (fin ^ fin1) & ( fin <> {} implies ( 1 <= len fin & len fin1 < len (fin1 ^ fin) ) ) )