let N be with_zero set ; :: thesis: for S being with_non-empty_values Mem-Struct over N
for p being FinPartState of S holds p in FinPartSt S
let S be with_non-empty_values Mem-Struct over N; :: thesis: for p being FinPartState of S holds p in FinPartSt S
let p be FinPartState of S; :: thesis: p in FinPartSt S
p in sproduct (the_Values_of S) by CARD_3:103;
hence p in FinPartSt S ; :: thesis: verum