let I be non empty set ; :: thesis: for a, b, c being set
for i being Element of I holds
( c in (i -singleton a) . b iff ( b = i & c = a ) )
let a, b, c be set ; :: thesis: for i being Element of I holds
( c in (i -singleton a) . b iff ( b = i & c = a ) )
let i be Element of I; :: thesis: ( c in (i -singleton a) . b iff ( b = i & c = a ) )
A1: ( (i -singleton a) . i = {a} & ( for b being set st b in I & b <> i holds
(i -singleton a) . b = {} ) ) by AOFA_A00:6;
dom (i -singleton a) = I by PARTFUN1:def 2;
then A2: for b being set st b nin I holds
(i -singleton a) . b = {} by FUNCT_1:def 2;

hereby :: thesis: ( b = i & c = a implies c in (i -singleton a) . b )

assume A3: c in (i -singleton a) . b ; :: thesis: ( b = i & c = a )
thus b = i by A3, A1, A2; :: thesis: c = a
hence c = a by A1, A3, TARSKI:def 1; :: thesis: verum

end;

thus ( b = i & c = a implies c in (i -singleton a) . b ) by A1, TARSKI:def 1; :: thesis: verum