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;