let N be with_zero set ; :: thesis: for S being with_non-empty_values Mem-Struct over N
for p being Element of FinPartSt S holds p is FinPartState of S
let S be with_non-empty_values Mem-Struct over N; :: thesis: for p being Element of FinPartSt S holds p is FinPartState of S
let p be Element of FinPartSt S; :: thesis: p is FinPartState of S
p in FinPartSt S ;
then ex q being Element of sproduct (the_Values_of S) st
( q = p & q is finite ) ;
hence p is FinPartState of S ; :: thesis: verum