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:87, FUNCT_2:65; :: 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 by FUNCT_2:def 1;
hence Empty^2-to-zero . x,x = 0 by FUNCT_1:def 4; :: thesis: verum

end;

end;