is mentioned by

Thm* l:Collection(T) List, x:T List. x col_list_prod(l) ||x|| = ||l|| & (i:. i < ||x|| x[i] l[i])	[member_col_list_prod]
Def col_list_prod(l)(x) == ||x|| = ||l|| & (i:. i < ||x|| x[i] l[i])	[col_list_prod]

Try larger context: GenAutomata