let V be set ; :: thesis: for C being finite set
for A being Element of Fin (PFuncs V,C) holds Involved A is finite
let C be finite set ; :: thesis: for A being Element of Fin (PFuncs V,C) holds Involved A is finite
let A be Element of Fin (PFuncs V,C); :: thesis: Involved A is finite

per cases ( not A is empty or A is empty ) ;

suppose not A is empty ; :: thesis: Involved A is finite

hence Involved A is finite by Lm2; :: thesis: verum

end;

suppose A is empty ; :: thesis: Involved A is finite

hence Involved A is finite by Th11; :: thesis: verum

end;

end;