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 set such that
A2: x in Involved A by XBOOLE_0:def 1;
consider f being finite Function such that
A3: ( f in A & x in dom f ) by A2, Def1;
thus contradiction by A1, A3; :: thesis: verum