let V be set ; :: thesis: 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 )
let C be finite set ; :: thesis: 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 )
let A, B be Element of Fin (PFuncs V,C); :: thesis: 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 )
let s be set ; :: thesis: ( s in A =>> B implies 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 ) )
assume s in A =>> B ; :: thesis: 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 )
then s in { (union { ((f . i) \ i) where i is Element of PFuncs V,C : i in A } ) where f is Element of PFuncs A,B : dom f = A } by XBOOLE_0:def 4;
then consider f being Element of PFuncs A,B such that
A1: s = union { ((f . i) \ i) where i is Element of PFuncs V,C : i in A } and
A2: dom f = A ;
f is PartFunc of A,B by PARTFUN1:121;
hence 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 ) by A1, A2; :: thesis: verum