let z be set ; :: thesis: ( <*z*> |-- z = {} & <*z*> -| z = {} )
z in {z} by TARSKI:def 1;
then A1: z in rng <*z*> by FINSEQ_1:56;
A2: ( z .. <*z*> = 1 & len <*z*> = 1 ) by Th22, FINSEQ_1:56;
hence <*z*> |-- z = {} by A1, FINSEQ_4:64; :: thesis: <*z*> -| z = {}
thus <*z*> -| z = {} by A1, A2, FINSEQ_4:52; :: thesis: verum