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