let x be set ; :: thesis: {x} is finite
set p = {{} } --> x;
A1: dom ({{} } --> x) = {{} } by FUNCOP_1:19;
take {{} } --> x ; :: according to FINSET_1:def 1 :: thesis: ( rng ({{} } --> x) = {x} & dom ({{} } --> x) in omega )
for y being set holds
( y in {x} iff ex x being set st
( x in dom ({{} } --> x) & y = ({{} } --> x) . x ) )

proof

let y be set ; :: thesis: ( y in {x} iff ex x being set st
( x in dom ({{} } --> x) & y = ({{} } --> x) . x ) )
thus ( y in {x} implies ex x being set st
( x in dom ({{} } --> x) & y = ({{} } --> x) . x ) ) :: thesis: ( ex x being set st
( x in dom ({{} } --> x) & y = ({{} } --> x) . x ) implies y in {x} )

proof

assume y in {x} ; :: thesis: ex x being set st
( x in dom ({{} } --> x) & y = ({{} } --> x) . x )
then A2: y = x by TARSKI:def 1;
take {} ; :: thesis: ( {} in dom ({{} } --> x) & y = ({{} } --> x) . {} )
thus {} in dom ({{} } --> x) by A1, TARSKI:def 1; :: thesis: y = ({{} } --> x) . {}
{} in {{} } by TARSKI:def 1;
hence y = ({{} } --> x) . {} by A2, FUNCOP_1:13; :: thesis: verum

end;

assume ex z being set st
( z in dom ({{} } --> x) & y = ({{} } --> x) . z ) ; :: thesis: y in {x}
then y = x by FUNCOP_1:13;
hence y in {x} by TARSKI:def 1; :: thesis: verum

end;

hence rng ({{} } --> x) = {x} by FUNCT_1:def 5; :: thesis: dom ({{} } --> x) in omega
thus dom ({{} } --> x) in omega by A1, ORDINAL3:18; :: thesis: verum