take f = id S; :: thesis: f is idempotent
f * f = f by FUNCT_2:23;
hence f is idempotent by QUANTAL1:def 9; :: thesis: verum