let V be set ; :: thesis: for C being finite set
for A, B being Element of Fin (PFuncs (V,C)) st A = {} & B <> {} holds
B =>> A = {}
let C be finite set ; :: thesis: for A, B being Element of Fin (PFuncs (V,C)) st A = {} & B <> {} holds
B =>> A = {}
let A, B be Element of Fin (PFuncs (V,C)); :: thesis: ( A = {} & B <> {} implies B =>> A = {} )
assume A1: ( A = {} & B <> {} ) ; :: thesis: B =>> A = {}
assume B =>> A <> {} ; :: thesis: contradiction
then consider k being object such that
A2: k in B =>> A by XBOOLE_0:def 1;
ex f being PartFunc of B,A st
( k = union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in B } & dom f = B ) by A2, HEYTING2:15;
hence contradiction by A1; :: thesis: verum