theorem :: CLASSES4:70

for X being empty set
for f being FinSequence of X * holds f = (len f) |-> 0 by FUNCT_7:17, MSSUBLAT:5;