for i being object st i in I holds
not ((Funcs) (A,A)) . i is empty

proof

let i be object ; :: thesis: ( i in I implies not ((Funcs) (A,A)) . i is empty )
assume A1: i in I ; :: thesis: not ((Funcs) (A,A)) . i is empty
then (id A) . i is Function of (A . i),(A . i) by PBOOLE:def 15;
then (id A) . i in Funcs ((A . i),(A . i)) by FUNCT_2:9;
hence not ((Funcs) (A,A)) . i is empty by A1, PBOOLE:def 17; :: thesis: verum

end;

hence (Funcs) (A,A) is non-empty by PBOOLE:def 13; :: thesis: verum