let V be set ; :: thesis: for C being finite set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
Involved A = {}
let C be finite set ; :: thesis: for A being Element of Fin (PFuncs (V,C)) st A = {} holds
Involved A = {}
let A be Element of Fin (PFuncs (V,C)); :: thesis: ( A = {} implies Involved A = {} )
assume A1: A = {} ; :: thesis: Involved A = {}
assume Involved A <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in Involved A by XBOOLE_0:def 1;
ex f being finite Function st
( f in A & x in dom f ) by A2, Def1;
hence contradiction by A1; :: thesis: verum