let x be set ; :: thesis: Empty^2-to-zero . (x,x) = 0
per cases ( [x,x] in [:1,1:] or not [x,x] in [:1,1:] ) ;
suppose [x,x] in [:1,1:] ; :: thesis: Empty^2-to-zero . (x,x) = 0
hence Empty^2-to-zero . (x,x) = 0 by CARD_1:49, FUNCT_2:50; :: thesis: verum
end;
suppose not [x,x] in [:1,1:] ; :: thesis: Empty^2-to-zero . (x,x) = 0
then not [x,x] in dom Empty^2-to-zero ;
hence Empty^2-to-zero . (x,x) = 0 by FUNCT_1:def 2; :: thesis: verum
end;
end;