let A be non empty set ; :: thesis: for f being Function of A,(Fin A) holds
( f = singleton A iff for x being Element of A holds f . x = {x} )
let f be Function of A,(Fin A); :: thesis: ( f = singleton A iff for x being Element of A holds f . x = {x} )
thus ( f = singleton A implies for x being Element of A holds f . x = {x} ) by Def6; :: thesis: ( ( for x being Element of A holds f . x = {x} ) implies f = singleton A )
assume for x being Element of A holds f . x = {x} ; :: thesis: f = singleton A
then for x being object st x in A holds
f . x = {x} ;
hence f = singleton A by Def6; :: thesis: verum