for V being set
for C being finite set
for A, B being Element of Fin (PFuncs (V,C))
for s being set st s in A =>> B holds
ex f being PartFunc of A,B st
( s = union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } & dom f = A )