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:47;
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