let x be object ; :: thesis: {x} is finite
set p = {{}} --> x;
take {{}} --> x ; :: according to FINSET_1:def 1 :: thesis: ( rng ({{}} --> x) = {x} & dom ({{}} --> x) in omega )
for y being object holds
( y in {x} iff ex x being object st
( x in dom ({{}} --> x) & y = ({{}} --> x) . x ) )
proof
let y be object ; :: thesis: ( y in {x} iff ex x being object st
( x in dom ({{}} --> x) & y = ({{}} --> x) . x ) )
thus ( y in {x} implies ex x being object st
( x in dom ({{}} --> x) & y = ({{}} --> x) . x ) ) :: thesis: ( ex x being object st
( x in dom ({{}} --> x) & y = ({{}} --> x) . x ) implies y in {x} )
proof
assume y in {x} ; :: thesis: ex x being object 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 TARSKI:def 1; :: thesis: y = ({{}} --> x) . {}
{} in {{}} by TARSKI:def 1;
hence y = ({{}} --> x) . {} by A2, FUNCOP_1:7; :: thesis: verum
end;
assume ex z being object st
( z in dom ({{}} --> x) & y = ({{}} --> x) . z ) ; :: thesis: y in {x}
then y = x by FUNCOP_1:7;
hence y in {x} by TARSKI:def 1; :: thesis: verum
end;
hence rng ({{}} --> x) = {x} by FUNCT_1:def 3; :: thesis: dom ({{}} --> x) in omega
thus dom ({{}} --> x) in omega by ORDINAL3:15; :: thesis: verum