reconsider X = Funcs ({},{}) as non empty set ;
reconsider I = id 1 as 1 -defined Function ;
set f = [:1,X:] * [:X,{1}:];
set g = [:{1},X:] * [:X,{0}:];
set ff = 1 --> 1;
set gg = {1} --> 0;
B0: ( 1 --> 1 = [:1,X:] * [:X,{1}:] & {1} --> 0 = [:{1},X:] * [:X,{0}:] ) by FOMODEL0:73;
(I +* (1 --> 1)) +* ({1} --> 0) = (0,1) --> (1,0) by CARD_1:49;
hence {} tohilb = (0,1) --> (1,0) by B0; :: thesis: verum