for i being object st i in I holds

not ((Funcs) (A,A)) . i is empty

not ((Funcs) (A,A)) . i is empty

proof

hence
(Funcs) (A,A) is non-empty
by PBOOLE:def 13; :: thesis: verum
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;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