let I be non empty set ; :: thesis: for i, j being Element of I
for x being set holds
( (i -singleton x) . i = {x} & ( i <> j implies (i -singleton x) . j = {} ) )
let i, j be Element of I; :: thesis: for x being set holds
( (i -singleton x) . i = {x} & ( i <> j implies (i -singleton x) . j = {} ) )
let x be set ; :: thesis: ( (i -singleton x) . i = {x} & ( i <> j implies (i -singleton x) . j = {} ) )
dom (EmptyMS I) = I by PARTFUN1:def 2;
hence (i -singleton x) . i = {x} by FUNCT_7:31; :: thesis: ( i <> j implies (i -singleton x) . j = {} )
assume i <> j ; :: thesis: (i -singleton x) . j = {}
hence (i -singleton x) . j = (EmptyMS I) . j by FUNCT_7:32
.= {} ;
:: thesis: verum