let a be set ; :: thesis: canFS {a} = <*a*>
A1: len (canFS {a}) = card {a} by Def1
.= 1 by CARD_1:50 ;
rng (canFS {a}) = {a} by FUNCT_2:def 3;
hence canFS {a} = <*a*> by A1, FINSEQ_1:56; :: thesis: verum