reconsider f = {} as PartFunc of (FinPartSt S),(FinPartSt S) by RELSET_1:12;
take f ; :: thesis: f is data-only
let p be PartState of S; :: according to MEMSTR_0:def 17 :: thesis: ( p in dom f implies ( p is data-only & ( for q being PartState of S st q = f . p holds
q is data-only ) ) )
thus ( p in dom f implies ( p is data-only & ( for q being PartState of S st q = f . p holds
q is data-only ) ) ) ; :: thesis: verum