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